walther@59827: % into "root.tex" as created by "isabelle mkdir"
walther@60183: %  code from "llncs/samplepaper.tex" is inserted -- llncs NOT COMPATIBLE WITH package isabelle
walther@59827: 
walther@59827: \documentclass{article}
walther@59827: \usepackage{isabelle,isabellesym}
walther@59827: \usepackage{graphicx}
walther@59827: %\usepackage{hyperref}  %\url{...}  don't use together with isabelle,isabellesym
walther@59827: %\usepackage{breakurl}  %\url{...}  don't use together with isabelle,isabellesym
walther@59827: %\renewcommand\UrlFont{\color{blue}\rmfamily} % ..recommended by llncs/samplepaper.tex
walther@59827: %                                   but isabelle says ***   \UrlFont undefined.
walther@59827: 
walther@59827: % further packages required for unusual symbols (see also
walther@59827: % isabellesym.sty), use only when needed
walther@59827: 
walther@59827: %\usepackage{amssymb}
walther@59827:   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
walther@59827:   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
walther@59827:   %\<triangleq>, \<yen>, \<lozenge>
walther@59827: 
walther@59827: %\usepackage{eurosym}
walther@59827:   %for \<euro>
walther@59827: 
walther@59827: %\usepackage[only,bigsqcap]{stmaryrd}
walther@59827:   %for \<Sqinter>
walther@59827: 
walther@59827: %\usepackage{eufrak}
walther@59827:   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
walther@59827: 
walther@59827: %\usepackage{textcomp}
walther@59827:   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
walther@59827:   %\<currency>
walther@59827: 
walther@59827: % this should be the last package used
walther@59827: \usepackage{pdfsetup}
walther@59827: 
walther@59827: % urls in roman style, theory text in math-similar italics
walther@59827: \urlstyle{rm}
walther@59827: \isabellestyle{tt}  %better readable than {it}
walther@59827: 
walther@59827: % for uniform font size
walther@59827: %\renewcommand{\isastyle}{\isastyleminor}
walther@59827: 
walther@59827: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
walther@59827: \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
walther@59827: \def\LI{$\cal{LI}$}
walther@59827: 
walther@59827: \begin{document}
walther@59827: 
walther@59827: \title{Introduction to Lucas-Interpretation}
walther@59827: \author{Walther Neuper}
walther@59827: %\institute{Johannes Kepler University, Linz, Austria}
walther@59827: \maketitle
walther@59827: \vspace{2cm}
walther@59827: \tableofcontents
walther@59827: \newpage
walther@59827: 
walther@59827: % sane default for proof documents
walther@59827: \parindent 0pt\parskip 0.5ex
walther@59827: 
walther@59827: % generated text of all theories
walther@59827: \input{Lucas_Interpreter.tex}  %*.tex created by isabelle build
walther@59827: 
walther@59827: % optional bibliography
walther@59827: \bibliographystyle{plain}
walther@59827: % \bibliographystyle{splncs04}
walther@59827: % splncs04 CAUSES ERROR
walther@59827: % SEE ~/material/templates/llncs/README
walther@59827: \bibliography{root}
walther@59827: 
walther@59827: \end{document}
walther@59827: 
walther@59827: %%% Local Variables:
walther@59827: %%% mode: latex
walther@59827: %%% TeX-master: t
walther@59827: %%% End: