diff --git a/thys/Epistemic_Logic/document/root.tex b/thys/Epistemic_Logic/document/root.tex
--- a/thys/Epistemic_Logic/document/root.tex
+++ b/thys/Epistemic_Logic/document/root.tex
@@ -1,46 +1,48 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 
+\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}
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
 \begin{document}
 
 \title{Epistemic Logic}
 \author{Asta Halkjær From}
 \maketitle
 
 \begin{abstract}
   This work is a formalization of epistemic logic with countably many agents.
   It includes proofs of soundness and completeness for the axiom system K.
   The completeness proof is based on the textbook ``Reasoning About Knowledge''
   by Fagin, Halpern, Moses and Vardi (MIT Press 1995)~\cite{fagin1995}.
 \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: