diff --git a/thys/Hermite_Lindemann/document/root.tex b/thys/Hermite_Lindemann/document/root.tex
--- a/thys/Hermite_Lindemann/document/root.tex
+++ b/thys/Hermite_Lindemann/document/root.tex
@@ -1,63 +1,64 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
+\usepackage[T1]{fontenc}
 \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{it}
 
 \begin{document}
 
 \title{The Hermite--Lindemann--Weierstraß Transcendence Theorem}
 \author{Manuel Eberl}
 \maketitle
 
 \begin{abstract}
 This article provides a formalisation of the Her\-mite\--Lin\-de\-mann\--Wei\-er\-straß Theorem
 (also known as simply Her\-mite\--Lin\-de\-mann or Lin\-de\-mann\--Wei\-er\-straß).
  This theorem is one of the crowning achievements of 19th century number theory.
 
 The theorem states that if $\alpha_1, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that
 are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$ are
 algebraically independent over $\mathbb{Q}$.
 
 Like the previous formalisation in Coq by Bernard~\cite{bernard}, I proceeded by formalising 
 Baker's alternative formulation of the theorem~\cite{baker} and then deriving the original one from
 that. Baker's version states that for any algebraic numbers
 $\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers
 $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have:
 \[\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0 \quad\quad\text{iff}\quad\quad
   \forall i.\ \beta_i = 0\]
 
 This has a number of immediate corollaries, e.g.:
 \begin{itemize}
 \item $e$ and $\pi$ are transcendental
 \item $e^z$, $\sin z$, $\tan z$, etc.\ are transcendental for algebraic $z\in\mathbb{C}\setminus\{0\}$
 \item $\ln z$ is transcendental for algebraic $z\in\mathbb{C}\setminus\{0, 1\}$
 \end{itemize}
 \end{abstract}
 
 \newpage
 \tableofcontents
 \newpage
 \parindent 0pt\parskip 0.5ex
 
 \input{session}
 
 \nocite{baker}
 \nocite{redheffer_steinberg}
 \nocite{bernard}
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
diff --git a/thys/Mereology/document/root.tex b/thys/Mereology/document/root.tex
--- a/thys/Mereology/document/root.tex
+++ b/thys/Mereology/document/root.tex
@@ -1,61 +1,62 @@
 \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{Mereology}
 \author{Ben Blumson}
 \maketitle
 
 \abstract{We use Isabelle/HOL to verify elementary theorems and alternative axiomatizations of classical extensional mereology.}
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 % optional bibliography
 \bibliographystyle{apalike}
 \bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
diff --git a/thys/Modular_arithmetic_LLL_and_HNF_algorithms/document/root.tex b/thys/Modular_arithmetic_LLL_and_HNF_algorithms/document/root.tex
--- a/thys/Modular_arithmetic_LLL_and_HNF_algorithms/document/root.tex
+++ b/thys/Modular_arithmetic_LLL_and_HNF_algorithms/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{Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation\footnote{Supported
 by FWF (Austrian Science Fund) project Y757 
 and by project MTM2017-88804-P (Spanish Ministry of Science and Innovation).}}
 %\title{Modulo arithmetic-based algorithms for lattice basis reduction and for computing the Hermite normal form}
 \author{Ralph Bottesch \and Jose Divas\'on \and Ren\'e Thiemann}
 \maketitle
 
 \begin{abstract}
 We verify two algorithms for which modular arithmetic plays an essential role: Storjohann's variant of the LLL lattice basis reduction algorithm and Kopparty's algorithm for computing the Hermite normal form of a matrix. To do this, we also formalize some facts about the modulo operation with symmetric range. Our implementations are based on the original papers, but are otherwise efficient. For basis reduction we formalize two versions: one that includes all of the optimizations/heuristics from Storjohann's paper, and one excluding a heuristic that we observed to often decrease efficiency. We also provide a fast, self-contained certifier for basis reduction, based on the efficient Hermite normal form algorithm.
 \end{abstract}
 
 \tableofcontents
 
 % 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/Projective_Measurements/document/root.tex b/thys/Projective_Measurements/document/root.tex
--- a/thys/Projective_Measurements/document/root.tex
+++ b/thys/Projective_Measurements/document/root.tex
@@ -1,59 +1,60 @@
 \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{Projective-Measurements}
 \author{Mnacho}
 \maketitle
 
 \tableofcontents
 
 % 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/Sunflowers/document/root.tex b/thys/Sunflowers/document/root.tex
--- a/thys/Sunflowers/document/root.tex
+++ b/thys/Sunflowers/document/root.tex
@@ -1,36 +1,37 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 
 \usepackage{amsmath}
 \usepackage{amssymb}
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 
 \begin{document}
 
 \title{The Sunflower Lemma of Erdős and Rado}
 \author{René Thiemann}
 \maketitle
 
 \begin{abstract}
 We formally define sunflowers and provide a formalization of
 the sunflower lemma of Erdős and Rado: whenever a set of size-$k$-sets has a larger cardinality 
 than $(r - 1)^k \cdot k!$, then it contains a sunflower of cardinality $r$.
 \end{abstract}
 
 % include generated text of all theories
 \input{session}
 
 % optional bibliography
 %\addcontentsline{toc}{section}{Bibliography}
 %\nocite{*}
 \bibliographystyle{plain}
 \bibliography{root}
 
 \end{document}