diff --git a/thys/Budan_Fourier/document/root.tex b/thys/Budan_Fourier/document/root.tex
--- a/thys/Budan_Fourier/document/root.tex
+++ b/thys/Budan_Fourier/document/root.tex
@@ -1,39 +1,43 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{amsmath}
-\usepackage{amssymb} 
+\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 Budan-Fourier Theorem and Counting Real Roots with Multiplicity}
 \author{Wenda Li}
 \maketitle
 
 \begin{abstract}
 	This entry is mainly about counting and approximating real roots (of a polynomial) with multiplicity.
 	We have first formalised the Budan-Fourier theorem: given a polynomial with real coefficients, we can calculate sign variations on Fourier sequences to over-approximate the number of real roots (counting multiplicity) within an interval. When all roots are known to be real, the over-approximation becomes tight: we can utilise this theorem to count real roots exactly. It is also worth noting that Descartes' rule of sign is a direct consequence of the Budan-Fourier theorem, and has been included in this entry. In addition, we have extended previous formalised Sturm's theorem to count real roots with multiplicity, while the original Sturm's theorem only counts distinct real roots. Compared to the Budan-Fourier theorem, our extended Sturm's theorem always counts roots exactly but may suffer from greater computational cost.
 \end{abstract}
 
 Many problems in real algebraic geometry is about counting or approximating roots of a polynomial. Previous formalised results are mainly about counting distinct real roots (i.e. Sturm's theorem in Isabelle/HOL \cite{Sturm_Tarski-AFP,Sturm_Sequences-AFP}, HOL Light \cite{harrison-poly}, PVS \cite{Narkawicz:2015do} and Coq \cite{Mahboubi:2012gg}) and limited support for multiple real roots (i.e. Descartes' rule of signs in Isabelle/HOL \cite{Descartes_Sign_Rule-AFP}, HOL Light and ProofPower\footnote{According to Freek Wiedijk's "Formalising 100 Theorems" (\url{http://www.cs.ru.nl/~freek/100/index.html})}). In comparison, this entry provides more comprehensive support for reasoning about multiple real roots.
 
 The main motivation of this entry is to cope with the roots-on-the-border issue when counting complex roots \cite{li_evaluate_cauchy,Count_Complex_Roots-AFP}, but the results here should be beneficial to other developments.
 
 Our proof of the Budan-Fourier theorem mainly follows Theorem 2.35 in the book by Basu et al. \cite{Basu:2006bo} and that of the extended Sturm's theorem is inspired by Theorem 10.5.6 in Rahman and Schmeisser's book \cite{Rahman:2016us}.
 
 %\tableofcontents
 
 % include generated text of all theories
 \input{session}
 
+\section{Acknowledgements}
+The work was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178), funded by the European Research Council
+and led by Professor Lawrence Paulson at the University of Cambridge, UK.
+
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
diff --git a/thys/Count_Complex_Roots/document/root.tex b/thys/Count_Complex_Roots/document/root.tex
--- a/thys/Count_Complex_Roots/document/root.tex
+++ b/thys/Count_Complex_Roots/document/root.tex
@@ -1,32 +1,36 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{amsmath}
-\usepackage{amssymb} 
+\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{Count the Number of Complex Roots}
 \author{Wenda Li}
 \maketitle
 
 \begin{abstract}
   Based on evaluating Cauchy indices through remainder sequences \cite{eisermann2012fundamental} \cite[Chapter 11]{rahman2002analytic}, this entry provides an effective procedure to count the number of complex roots (with multiplicity) of a polynomial within a rectangle box or a half-plane. Potential applications of this entry include certified complex root isolation (of a polynomial) and testing the Routh-Hurwitz stability criterion (i.e., to check whether all the roots of some characteristic polynomial have negative real parts).
 \end{abstract}
 
 %\tableofcontents
 
 % include generated text of all theories
 \input{session}
 
+\section{Acknowledgements}
+The work was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178), funded by the European Research Council
+and led by Professor Lawrence Paulson at the University of Cambridge, UK.
+
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
diff --git a/thys/Fourier/document/root.tex b/thys/Fourier/document/root.tex
--- a/thys/Fourier/document/root.tex
+++ b/thys/Fourier/document/root.tex
@@ -1,43 +1,47 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{mathtools,url}
 \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}
 
 \bibliographystyle{plain}
 
 \begin{document}
 
 \title{Fourier Series}
 \author{Lawrence C Paulson}
 \date{}
 \maketitle
 
 \begin{abstract}
 This development formalises the square integrable functions over the reals and the basics of Fourier series. It culminates with a proof that every well-behaved periodic function can be approximated by a Fourier series. The material is ported from HOL Light.\footnote{\url{https://github.com/jrh13/hol-light/blob/master/100/fourier.ml}}
 \end{abstract}
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
+
+\section{Acknowledgements}
+The author was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council.
+
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
diff --git a/thys/Green/document/root.tex b/thys/Green/document/root.tex
--- a/thys/Green/document/root.tex
+++ b/thys/Green/document/root.tex
@@ -1,39 +1,43 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb,amsmath}
 
 % 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{An Isabelle/HOL formalisation of Green's Theorem}
 \author{Mohammad Abdulaziz and Lawrence C.\ Paulson}
 \maketitle
 
 \begin{abstract}
   We formalise a statement of Green’s theorem—the first formalisation to
   our knowledge—in Isabelle/HOL. The theorem statement that we formalise
   is enough for most applications, especially in physics and
   engineering. Our formalisation is made possible by a novel proof that
   avoids the ubiquitous line integral cancellation argument. This
   eliminates the need to formalise orientations and region boundaries
   explicitly with respect to the outwards-pointing normal vector.
   Instead we appeal to a homological argument about equivalences between
   paths.
 \end{abstract}
 
 % \tableofcontents
 
+\section{Acknowledgements}
+Paulson was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council
+at the University of Cambridge, UK.
+
 % include generated text of all theories
 \input{session}
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
diff --git a/thys/Prime_Number_Theorem/document/root.tex b/thys/Prime_Number_Theorem/document/root.tex
--- a/thys/Prime_Number_Theorem/document/root.tex
+++ b/thys/Prime_Number_Theorem/document/root.tex
@@ -1,43 +1,46 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{amsfonts, amsmath, 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 Prime Number Theorem}
 \author{Manuel Eberl and Larry Paulson}
 \maketitle
 
 \begin{abstract}
 This article provides a short proof of the Prime Number Theorem in several equivalent forms, most notably $\pi(x)\sim x / \ln x$ where $\pi(x)$ is the number of primes no larger than $x$. It also defines other basic number-theoretic functions related to primes like Chebyshev's $\vartheta$ and $\psi$ and the ``$n$-th prime number'' function $p_n$. We also show various bounds and relationship between these functions are shown. Lastly, we derive Mertens' First and Second Theorem, i.\,e.\ $\sum_{p\leq x} \frac{\ln p}{p} = \ln x + O(1)$ and $\sum_{p\leq x} \frac{1}{p} = \ln\ln x + M + O(1/\ln x)$. We also give explicit bounds for the remainder terms.
 
 The proof of the Prime Number Theorem builds on a library of Dirichlet series and analytic combinatorics. We essentially follow the presentation by Newman~\cite{newman1998analytic}. The core part of the proof is a Tauberian theorem for Dirichlet series, which is proven using complex analysis and then used to strengthen Mertens' First Theorem to $\sum_{p\leq x} \frac{\ln p}{p} = \ln x + c + o(1)$.
 
 A variant of this proof has been formalised before by Harrison in HOL Light~\cite{harrison-pnt}, and formalisations of Selberg's elementary proof exist both by Avigad \textit{et al.}\ \cite{avigad_pnt}\ in Isabelle and by Carneiro~\cite{carneiro_pnt} in Metamath.
 The advantage of the analytic proof is that, while it requires more powerful mathematical tools, it is considerably shorter and clearer. This article attempts to provide a short and clear formalisation of all components of that proof using the full range of mathematical machinery available in Isabelle, staying as close as possible to Newman's simple paper proof.
 \end{abstract}
 
 \newpage
 \tableofcontents
 \newpage
 \parindent 0pt\parskip 0.5ex
 
 \input{session}
 
+\section{Acknowledgements}
+Paulson was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council at the University of Cambridge, UK.
+
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
diff --git a/thys/Quaternions/document/root.tex b/thys/Quaternions/document/root.tex
--- a/thys/Quaternions/document/root.tex
+++ b/thys/Quaternions/document/root.tex
@@ -1,33 +1,36 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{amsmath,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{Quaternions}
 \author{Lawrence C. Paulson}
 \maketitle
 
 \begin{abstract}
 This theory is inspired by the HOL Light development of quaternions~\cite{gabrielli-quaternions}, but follows its own route. Quaternions are developed coinductively, as in the existing formalisation of the complex numbers. Quaternions are quickly shown to belong to the type classes of real normed division algebras and real inner product spaces. And therefore they inherit a great body of facts involving algebraic laws, limits, continuity, etc., which must be proved explicitly in the HOL Light version. The development concludes with the geometric interpretation of the product of imaginary quaternions.
 
 
 \end{abstract}
 
 \tableofcontents
 
 % include generated text of all theories
 \input{session}
 
+\section{Acknowledgements}
+The author was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council.
+
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
diff --git a/thys/Winding_Number_Eval/document/root.tex b/thys/Winding_Number_Eval/document/root.tex
--- a/thys/Winding_Number_Eval/document/root.tex
+++ b/thys/Winding_Number_Eval/document/root.tex
@@ -1,32 +1,36 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{amsmath}
-\usepackage{amssymb} 
+\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{Evaluate Winding Numbers through Cauchy Indices}
 \author{Wenda Li}
 \maketitle
 
 \begin{abstract}
 	In complex analysis, the winding number measures the number of times a path (counterclockwise) winds around a point, while the Cauchy index can approximate how the path winds. This entry provides a formalisation of the Cauchy index, which is then shown to be related to the winding number. In addition, this entry also offers a tactic that enables users to evaluate the winding number by calculating Cauchy indices. The connection between the winding number and the Cauchy index can be found in the literature \cite{eisermann2012fundamental} \cite[Chapter 11]{rahman2002analytic}.
 \end{abstract}
 
 %\tableofcontents
 
 % include generated text of all theories
 \input{session}
 
+\section{Acknowledgements}
+The work was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178), funded by the European Research Council
+and led by Professor Lawrence Paulson at the University of Cambridge, UK.
+
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
diff --git a/thys/ZFC_in_HOL/document/root.tex b/thys/ZFC_in_HOL/document/root.tex
--- a/thys/ZFC_in_HOL/document/root.tex
+++ b/thys/ZFC_in_HOL/document/root.tex
@@ -1,61 +1,64 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 
 \usepackage{amssymb}
 \usepackage{stmaryrd}
 
 % 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{Zermelo Fraenkel Set Theory in Higher-Order Logic}
 \author{Lawrence C. Paulson\\ Computer Laboratory\\ University of Cambridge}
 
 \maketitle
 
 \begin{abstract}
 This entry is a new formalisation of ZFC set theory in Isabelle/HOL\@.
 It is logically equivalent to Obua's HOLZF~\cite{obua-partizan-games}; the point is to have the closest possible integration
 with the rest of Isabelle/HOL, minimising the amount of new notations and exploiting type classes.
 
-There is a type \isa{V} of sets and a function 
+There is a type \isa{V} of sets and a function
 \isa{elts :: V\ {\isasymRightarrow}\ V\ set} mapping a set to its elements.
 Classes simply have type \isa{V\ set}, and the predicate \isa{small} identifies those classes that correspond to actual sets.
 Type classes connected with orders and lattices are used to minimise the amount of new notation
 for concepts such as the subset relation, union and intersection.
 Basic concepts are formalised: Cartesian products, disjoint sums, natural numbers, functions, etc.
 
 More advanced set-theoretic concepts, such as transfinite induction, ordinals, cardinals
 and the transitive closure of a set, are also provided.
 The definition of addition and multiplication for general sets (not just ordinals) follows Kirby \cite{kirby-addition}.
 The development includes essential results about cardinal arithmetic. It also develops ordinal exponentiation, Cantor normal form and the concept of indecomposable ordinals. There are numerous results about order types.
 
 The theory provides two type classes with the aim of
 facilitating developments that combine \isa{V} with other Isabelle/HOL types:
 \isa{embeddable}, the class of types that can be injected into~\isa{V} (including \isa{V} itself as well as \isa{V*V}, \isa{V\ list}, etc.), and
 \isa{small}, the class of types that correspond to some ZF set.
 \end{abstract}
 
 \newpage
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \newpage
 \input{session}
 
+\section{Acknowledgements}
+The author was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council.
+
 \bibliographystyle{abbrv}
 \bibliography{root.bib}
 
 \end{document}