1.1 --- a/src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex	Sun Apr 04 12:29:42 2021 +0200
     1.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex	Sun Apr 04 13:31:04 2021 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  % into "root.tex" as created by "isabelle mkdir"
     1.5 -%  code from "llncs/samplepaper.tex" is inserted
     1.6 +%  code from "llncs/samplepaper.tex" is inserted -- llncs NOT COMPATIBLE WITH package isabelle
     1.7  
     1.8  \documentclass{article}
     1.9  \usepackage{isabelle,isabellesym}

     2.1 --- a/src/Tools/isac/Doc/README	Sun Apr 04 12:29:42 2021 +0200
     2.2 +++ b/src/Tools/isac/Doc/README	Sun Apr 04 13:31:04 2021 +0200
     2.3 @@ -4,4 +4,4 @@
     2.4  /usr/local/isabisac/bin/isabelle build -D .
     2.5   
     2.6  In case nothing happens with the above command, go
     2.7 -~/.isabelle/isabisac/heaps/polyml-5.8_x86_64_32-linux/log$ rm Lucas_Interpreter*
     2.8 +~/.isabelle/isabisac/heaps/polyml-5.8_x86_64_32-linux/log$ rm Interpret*

     3.1 --- a/src/Tools/isac/Doc/ROOT	Sun Apr 04 12:29:42 2021 +0200
     3.2 +++ b/src/Tools/isac/Doc/ROOT	Sun Apr 04 13:31:04 2021 +0200
     3.3 @@ -14,3 +14,17 @@
     3.4      "fun-pack-simplify.png"
     3.5      "root.bib"
     3.6      "root.tex"
     3.7 +
     3.8 +session "Specify_Phase" in "Specify_Phase" = HOL +
     3.9 +  options [document = pdf, document_output = "output"]
    3.10 +  sessions
    3.11 +    "Specify"
    3.12 +  theories
    3.13 +    "Specify_Phase"
    3.14 +  document_files (in "../")
    3.15 +    "isabelle.sty"
    3.16 +    "isabellesym.sty"
    3.17 +    "pdfsetup.sty"
    3.18 +  document_files
    3.19 +    "root.bib"
    3.20 +    "root.tex"

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Sun Apr 04 13:31:04 2021 +0200
     4.3 @@ -0,0 +1,11 @@
     4.4 +(*<*)
     4.5 +(*%:wrap=soft:maxLineLen=78:*)
     4.6 +theory Specify_Phase
     4.7 +  imports "Specify.Specify"
     4.8 +begin
     4.9 +(*>*)
    4.10 +
    4.11 +
    4.12 +(*<*)
    4.13 +end
    4.14 +(*>*)
    4.15 \ No newline at end of file

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/root.bib	Sun Apr 04 13:31:04 2021 +0200
     5.3 @@ -0,0 +1,8 @@
     5.4 +@TechReport{isac:all,
     5.5 +  author = 	 {\isac{}- Team},
     5.6 +  title = 	 {\isac{} -- User Requirements Document},
     5.7 +  institution =  {Institute for Softwaretechnology, 
     5.8 +                  University of Technology},
     5.9 +  year = 	 {2002},
    5.10 +  note = 	 {\url{https://static.miraheze.org/isacwiki/TODO/URD.pdf}}
    5.11 +}

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Sun Apr 04 13:31:04 2021 +0200
     6.3 @@ -0,0 +1,45 @@
     6.4 +\documentclass{article}
     6.5 +\usepackage{isabelle,isabellesym}
     6.6 +\usepackage{graphicx}
     6.7 +% this should be the last package used
     6.8 +\usepackage{pdfsetup}
     6.9 +
    6.10 +% urls in roman style, theory text in math-similar italics
    6.11 +\urlstyle{rm}
    6.12 +\isabellestyle{tt}  %better readable than {it}
    6.13 +
    6.14 +% for uniform font size
    6.15 +%\renewcommand{\isastyle}{\isastyleminor}
    6.16 +
    6.17 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    6.18 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    6.19 +
    6.20 +\begin{document}
    6.21 +
    6.22 +\title{The Specify Phase in \isac's Calculations}
    6.23 +\author{Walther Neuper}
    6.24 +%\institute{Johannes Kepler University, Linz, Austria}
    6.25 +\maketitle
    6.26 +\vspace{2cm}
    6.27 +\tableofcontents
    6.28 +\newpage
    6.29 +
    6.30 +% sane default for proof documents
    6.31 +\parindent 0pt\parskip 0.5ex
    6.32 +
    6.33 +% generated text of all theories
    6.34 +\input{Specify_Phase.tex}  %*.tex created by isabelle build
    6.35 +
    6.36 +% optional bibliography
    6.37 +\bibliographystyle{plain}
    6.38 +% \bibliographystyle{splncs04}
    6.39 +% splncs04 CAUSES ERROR
    6.40 +% SEE ~/material/templates/llncs/README
    6.41 +\bibliography{root}
    6.42 +
    6.43 +\end{document}
    6.44 +
    6.45 +%%% Local Variables:
    6.46 +%%% mode: latex
    6.47 +%%% TeX-master: t
    6.48 +%%% End: