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 \, \, \, \, \, \,
%\, \, \, \, \,
%\, \, \
%\usepackage{eurosym}
%for \
%\usepackage[only,bigsqcap]{stmaryrd}
%for \
%\usepackage{eufrak}
%for \ ... \, \ ... \ (also included in amssymb)
%\usepackage{textcomp}
%for \, \, \, \, \,
%\
% 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: