diff --git a/thys/Hybrid_Logic/document/root.tex b/thys/Hybrid_Logic/document/root.tex
--- a/thys/Hybrid_Logic/document/root.tex
+++ b/thys/Hybrid_Logic/document/root.tex
@@ -1,91 +1,92 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[utf8]{inputenc}
 \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{Formalizing a Seligman-Style Tableau System for Hybrid Logic}
 \author{Asta Halkjær From}
 \maketitle
 
 \begin{abstract}
   This work is a formalization of soundness and completeness proofs for a Seligman-style tableau system for hybrid logic~\cite{jlog17}.
   The completeness result is obtained via a synthetic approach using maximally consistent sets of tableau blocks~\cite{aiml16}.
   The formalization differs from the cited work in a few ways.
   First, to avoid the need to backtrack in the construction of a tableau, the formalized system has no unnamed initial segment, and therefore no \textit{Name} rule.
   Second, I show that the full \textit{Bridge} rule is admissible in the system.
   Third, I start from rules restricted to only extend the branch with new formulas, including only witnessing diamonds that are not already witnessed, and show that the unrestricted rules are derivable.
   Similarly, I start from simpler versions of the \( @ \)-rules and derive the general ones.
   Finally, the \textit{GoTo} rule is restricted using a notion of coins such that each application consumes a coin and coins are earned through applications of the remaining rules.
   I show that if a branch can be closed then it can be closed starting from a single coin.
   These restrictions are imposed to rule out some means of nontermination~\cite{jlog17}.
 \end{abstract}
 
 \section*{Preamble}
 
 The formalization is part of the author's MSc thesis in Computer Science and Engineering at the Technical University of Denmark (DTU).
 
 \paragraph{Supervisors:}
 
 \begin{itemize}
   \item Jørgen Villadsen
   \item Alexander Birch Jensen (co-supervisor)
   \item Patrick Blackburn (Roskilde University, external supervisor)
 \end{itemize}
 
 \newpage
 \tableofcontents
 
 \newpage
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 \nocite{*}
 
 % optional bibliography
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \addcontentsline{toc}{section}{References}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End: