\documentclass{report}
\usepackage{isabelle,isabellesym}
\usepackage{graphicx}
\usepackage{paralist}  % compactitem
% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{tt}  %better readable than {it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
\def\see{$\rightarrow$}
\newtheorem{UR}{UR}[section]
\newtheorem{Expl}{Expl}[section]

\begin{document}

\title{The Specify Phase in \isac's Calculations}
\author{Walther Neuper}
%\institute{Johannes Kepler University, Linz, Austria}
\maketitle
\tableofcontents
\newpage

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

\nocite{*}  %FIXME satisfy bibtex without actual text + citations
\input{user-requirements.tex}

% generated text of all theories
\input{Specify_Phase.tex}  %*.tex created by isabelle build

% optional bibliography
\bibliographystyle{plain}
% \bibliographystyle{splncs04}
% splncs04 CAUSES ERROR
% SEE ~/material/templates/llncs/README
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
