1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex	Wed Mar 11 15:25:52 2020 +0100
     1.3 @@ -0,0 +1,75 @@
     1.4 +% into "root.tex" as created by "isabelle mkdir"
     1.5 +%  code from "llncs/samplepaper.tex" is inserted
     1.6 +
     1.7 +\documentclass{article}
     1.8 +\usepackage{isabelle,isabellesym}
     1.9 +\usepackage{graphicx}
    1.10 +%\usepackage{hyperref}  %\url{...}  don't use together with isabelle,isabellesym
    1.11 +%\usepackage{breakurl}  %\url{...}  don't use together with isabelle,isabellesym
    1.12 +%\renewcommand\UrlFont{\color{blue}\rmfamily} % ..recommended by llncs/samplepaper.tex
    1.13 +%                                   but isabelle says ***   \UrlFont undefined.
    1.14 +
    1.15 +% further packages required for unusual symbols (see also
    1.16 +% isabellesym.sty), use only when needed
    1.17 +
    1.18 +%\usepackage{amssymb}
    1.19 +  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
    1.20 +  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
    1.21 +  %\<triangleq>, \<yen>, \<lozenge>
    1.22 +
    1.23 +%\usepackage{eurosym}
    1.24 +  %for \<euro>
    1.25 +
    1.26 +%\usepackage[only,bigsqcap]{stmaryrd}
    1.27 +  %for \<Sqinter>
    1.28 +
    1.29 +%\usepackage{eufrak}
    1.30 +  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
    1.31 +
    1.32 +%\usepackage{textcomp}
    1.33 +  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
    1.34 +  %\<currency>
    1.35 +
    1.36 +% this should be the last package used
    1.37 +\usepackage{pdfsetup}
    1.38 +
    1.39 +% urls in roman style, theory text in math-similar italics
    1.40 +\urlstyle{rm}
    1.41 +\isabellestyle{tt}  %better readable than {it}
    1.42 +
    1.43 +% for uniform font size
    1.44 +%\renewcommand{\isastyle}{\isastyleminor}
    1.45 +
    1.46 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    1.47 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    1.48 +\def\LI{$\cal{LI}$}
    1.49 +
    1.50 +\begin{document}
    1.51 +
    1.52 +\title{Introduction to Lucas-Interpretation}
    1.53 +\author{Walther Neuper}
    1.54 +%\institute{Johannes Kepler University, Linz, Austria}
    1.55 +\maketitle
    1.56 +\vspace{2cm}
    1.57 +\tableofcontents
    1.58 +\newpage
    1.59 +
    1.60 +% sane default for proof documents
    1.61 +\parindent 0pt\parskip 0.5ex
    1.62 +
    1.63 +% generated text of all theories
    1.64 +\input{Lucas_Interpreter.tex}  %*.tex created by isabelle build
    1.65 +
    1.66 +% optional bibliography
    1.67 +\bibliographystyle{plain}
    1.68 +% \bibliographystyle{splncs04}
    1.69 +% splncs04 CAUSES ERROR
    1.70 +% SEE ~/material/templates/llncs/README
    1.71 +\bibliography{root}
    1.72 +
    1.73 +\end{document}
    1.74 +
    1.75 +%%% Local Variables:
    1.76 +%%% mode: latex
    1.77 +%%% TeX-master: t
    1.78 +%%% End: