diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,75 @@
+% into "root.tex" as created by "isabelle mkdir"
+%  code from "llncs/samplepaper.tex" is inserted
+
+\documentclass{article}
+\usepackage{isabelle,isabellesym}
+\usepackage{graphicx}
+%\usepackage{hyperref}  %\url{...}  don't use together with isabelle,isabellesym
+%\usepackage{breakurl}  %\url{...}  don't use together with isabelle,isabellesym
+%\renewcommand\UrlFont{\color{blue}\rmfamily} % ..recommended by llncs/samplepaper.tex
+%                                   but isabelle says ***   \UrlFont undefined.
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap]{stmaryrd}
+  %for \<Sqinter>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% 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\LI{$\cal{LI}$}
+
+\begin{document}
+
+\title{Introduction to Lucas-Interpretation}
+\author{Walther Neuper}
+%\institute{Johannes Kepler University, Linz, Austria}
+\maketitle
+\vspace{2cm}
+\tableofcontents
+\newpage
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{Lucas_Interpreter.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: