diff --git a/thys/IMP_Compiler/document/root.tex b/thys/IMP_Compiler/document/root.tex
--- a/thys/IMP_Compiler/document/root.tex
+++ b/thys/IMP_Compiler/document/root.tex
@@ -1,68 +1,69 @@
 \documentclass[11pt,a4paper,fleqn]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \renewcommand{\isastyletxt}{\isastyletext}
 
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
 \usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   %\<triangleq>, \<yen>, \<lozenge>
 
 %\usepackage{eurosym}
   %for \<euro>
 
 %\usepackage[only,bigsqcap]{stmaryrd}
   %for \<Sqinter>
 
 %\usepackage{eufrak}
   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
 
 %\usepackage{textcomp}
   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   %\<currency>
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
 
 \begin{document}
 
 \title{A Shorter Compiler Correctness Proof\\for Language IMP}
 \author{Pasquale Noce\\Software Engineer at HID Global, Italy\\pasquale dot noce dot lavoro at gmail dot com\\pasquale dot noce at hidglobal dot com}
 \maketitle
 
 \begin{abstract}
 This paper presents a compiler correctness proof for the didactic imperative programming language
 IMP, introduced in Nipkow and Klein's book on formal programming language semantics (version of
 March 2021), whose size is just two thirds of the book's proof in the number of formal text lines.
 As such, it promises to constitute a further enhanced reference for the formal verification of
 compilers meant for larger, real-world programming languages.
 
 The presented proof does not depend on language determinism, so that the proposed approach can be
 applied to non-deterministic languages as well. As a confirmation, this paper extends IMP with an
 additional non-deterministic choice command, and proves compiler correctness, viz. the simulation of
 compiled code execution by source code, for such extended language.
 \end{abstract}
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 % bibliography
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
diff --git a/thys/MiniSail/document/root.tex b/thys/MiniSail/document/root.tex
--- a/thys/MiniSail/document/root.tex
+++ b/thys/MiniSail/document/root.tex
@@ -1,71 +1,72 @@
 \documentclass[11pt,a4paper]{report}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym}
 
 \usepackage[a4paper,includeheadfoot,margin=2.54cm]{geometry}
 
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
 \usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   %\<triangleq>, \<yen>, \<lozenge>
 
 %\usepackage{eurosym}
   %for \<euro>
 
 %\usepackage[only,bigsqcap]{stmaryrd}
   %for \<Sqinter>
 
 %\usepackage{eufrak}
   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
 
 %\usepackage{textcomp}
   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   %\<currency>
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
 \begin{document}
 
 \title{MiniSail}
 \author{Mark P. Wassell}
 \maketitle
 
 \begin{abstract}
 MiniSail is a kernel language for Sail~\cite{Armstrong2019}, 
 an instruction set architecture (ISA) specification language. 
 Sail is an imperative language with a light-weight dependent type system similar to refinement type systems such as~\cite{Vazou2014}.
 From an ISA specification, the Sail compiler can generate theorem prover code and C (or OCaml) to give an executable 
 emulator for an architecture.
 The idea behind MiniSail is to capture the key and novel features of Sail in terms of their syntax, 
 typing rules and operational semantics,
 and to confirm that they work together by proving progress and preservation lemmas. 
 We use the Nominal2 library to handle binding.
 \end{abstract}
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 \begin{center}
   \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
 \end{center}
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
 
diff --git a/thys/Public_Announcement_Logic/document/root.tex b/thys/Public_Announcement_Logic/document/root.tex
--- a/thys/Public_Announcement_Logic/document/root.tex
+++ b/thys/Public_Announcement_Logic/document/root.tex
@@ -1,66 +1,67 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
 %\usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   %\<triangleq>, \<yen>, \<lozenge>
 
 %\usepackage{eurosym}
   %for \<euro>
 
 %\usepackage[only,bigsqcap]{stmaryrd}
   %for \<Sqinter>
 
 %\usepackage{eufrak}
   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
 
 %\usepackage{textcomp}
   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   %\<currency>
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
 
 \begin{document}
 
 \title{Public Announcement Logic}
 \author{Asta Halkjær From}
 \maketitle
 
 \begin{abstract}
   This work is a formalization of public announcement logic with countably many agents.
   It includes proofs of soundness and completeness for a variant of the axiom system PA + DIST! + NEC!~\cite{WangC13}. The completeness proof builds on the Epistemic Logic theory.
 \end{abstract}
 
 \tableofcontents
 
 \newpage
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 % optional bibliography
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
diff --git a/thys/Van_der_Waerden/document/root.tex b/thys/Van_der_Waerden/document/root.tex
--- a/thys/Van_der_Waerden/document/root.tex
+++ b/thys/Van_der_Waerden/document/root.tex
@@ -1,44 +1,45 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{amsfonts, amsmath, amssymb}
 
 % this should be the last package used
 \usepackage{pdfsetup}
 \usepackage[shortcuts]{extdash}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{rm}
 
 
 \begin{document}
 
 \title{Van der Waerden's Theorem}
 \author{Katharina Kreuzer, Manuel Eberl}
 \maketitle
 
 \begin{abstract}
 This article formalises the proof of Van der Waerden's Theorem from Ramsey theory. 
 
 Van der Waerden's Theorem states that for integers $k$ and $l$ there exists a number $N$ which guarantees that if an integer interval of length at least $N$ is coloured with $k$ colours, there will always be an arithmetic progression of length $l$ of the same colour in said interval. 
 The proof goes along the lines of Swan~\cite{Swan}.
 
 The smallest number $N_{k,l}$ fulfilling Van der Waerden's Theorem is then called the Van der Waerden Number. Finding the Van der Waerden Number is still an open problem for most values of $k$ and~$l$.
 \end{abstract}
 
 
 \newpage
 \tableofcontents
 
 \newpage
 \parindent 0pt\parskip 0.5ex
 
 \input{session}
 
 \nocite{Swan}
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}