|
1 % into "root.tex" as created by "isabelle mkdir" |
|
2 % code from "llncs/samplepaper.tex" is inserted |
|
3 |
|
4 \documentclass{article} |
|
5 \usepackage{isabelle,isabellesym} |
|
6 \usepackage{graphicx} |
|
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. |
|
11 |
|
12 % further packages required for unusual symbols (see also |
|
13 % isabellesym.sty), use only when needed |
|
14 |
|
15 %\usepackage{amssymb} |
|
16 %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, |
|
17 %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, |
|
18 %\<triangleq>, \<yen>, \<lozenge> |
|
19 |
|
20 %\usepackage{eurosym} |
|
21 %for \<euro> |
|
22 |
|
23 %\usepackage[only,bigsqcap]{stmaryrd} |
|
24 %for \<Sqinter> |
|
25 |
|
26 %\usepackage{eufrak} |
|
27 %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb) |
|
28 |
|
29 %\usepackage{textcomp} |
|
30 %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>, |
|
31 %\<currency> |
|
32 |
|
33 % this should be the last package used |
|
34 \usepackage{pdfsetup} |
|
35 |
|
36 % urls in roman style, theory text in math-similar italics |
|
37 \urlstyle{rm} |
|
38 \isabellestyle{tt} %better readable than {it} |
|
39 |
|
40 % for uniform font size |
|
41 %\renewcommand{\isastyle}{\isastyleminor} |
|
42 |
|
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}$}} |
|
45 \def\LI{$\cal{LI}$} |
|
46 |
|
47 \begin{document} |
|
48 |
|
49 \title{Introduction to Lucas-Interpretation} |
|
50 \author{Walther Neuper} |
|
51 %\institute{Johannes Kepler University, Linz, Austria} |
|
52 \maketitle |
|
53 \vspace{2cm} |
|
54 \tableofcontents |
|
55 \newpage |
|
56 |
|
57 % sane default for proof documents |
|
58 \parindent 0pt\parskip 0.5ex |
|
59 |
|
60 % generated text of all theories |
|
61 \input{Lucas_Interpreter.tex} %*.tex created by isabelle build |
|
62 |
|
63 % optional bibliography |
|
64 \bibliographystyle{plain} |
|
65 % \bibliographystyle{splncs04} |
|
66 % splncs04 CAUSES ERROR |
|
67 % SEE ~/material/templates/llncs/README |
|
68 \bibliography{root} |
|
69 |
|
70 \end{document} |
|
71 |
|
72 %%% Local Variables: |
|
73 %%% mode: latex |
|
74 %%% TeX-master: t |
|
75 %%% End: |