1 % into "root.tex" as created by "isabelle mkdir"
2 % code from "llncs/samplepaper.tex" is inserted
4 \documentclass{article}
5 \usepackage{isabelle,isabellesym}
7 %\usepackage{hyperref} %\url{...} don't use together with isabelle,isabellesym
8 %\usepackage{breakurl} %\url{...} don't use together with isabelle,isabellesym
9 %\renewcommand\UrlFont{\color{blue}\rmfamily} % ..recommended by llncs/samplepaper.tex
10 % but isabelle says *** \UrlFont undefined.
12 % further packages required for unusual symbols (see also
13 % isabellesym.sty), use only when needed
16 %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
17 %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
18 %\<triangleq>, \<yen>, \<lozenge>
23 %\usepackage[only,bigsqcap]{stmaryrd}
27 %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
29 %\usepackage{textcomp}
30 %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
33 % this should be the last package used
36 % urls in roman style, theory text in math-similar italics
38 \isabellestyle{tt} %better readable than {it}
40 % for uniform font size
41 %\renewcommand{\isastyle}{\isastyleminor}
43 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
44 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
49 \title{Introduction to Lucas-Interpretation}
50 \author{Walther Neuper}
51 %\institute{Johannes Kepler University, Linz, Austria}
57 % sane default for proof documents
58 \parindent 0pt\parskip 0.5ex
60 % generated text of all theories
61 \input{Lucas_Interpreter.tex} %*.tex created by isabelle build
63 % optional bibliography
64 \bibliographystyle{plain}
65 % \bibliographystyle{splncs04}
66 % splncs04 CAUSES ERROR
67 % SEE ~/material/templates/llncs/README