1.1 --- a/src/Tools/isac/Doc/ROOT	Tue Apr 13 13:20:05 2021 +0200
     1.2 +++ b/src/Tools/isac/Doc/ROOT	Tue Apr 13 14:07:17 2021 +0200
     1.3 @@ -1,15 +1,11 @@
     1.4 -(*~~$ ./bin/isabelle build ???
     1.5 -*)
     1.6 +(*~~$ ./bin/isabelle build -v -b Lucas_Interpreter
     1.7 + *)
     1.8  session "Lucas_Interpreter" in "Lucas_Interpreter" = HOL +
     1.9    options [document = pdf, document_output = "output"]
    1.10    sessions
    1.11      "Interpret"
    1.12    theories
    1.13      "Lucas_Interpreter"
    1.14 -  document_files (in "../")
    1.15 -    "isabelle.sty"
    1.16 -    "isabellesym.sty"
    1.17 -    "pdfsetup.sty"
    1.18    document_files
    1.19      "bend-7-70-en.png"
    1.20      "fun-pack-biegelinie-2.png"
    1.21 @@ -17,19 +13,15 @@
    1.22      "root.bib"
    1.23      "root.tex"
    1.24  
    1.25 -(*~~$ ./bin/isabelle build -v -b -D ~~/src/Tools/isac/Doc/Specify_Phase
    1.26 -    *** Bad session root directory: "/usr/local/isabisac/src/Tools/isac/Doc/Specify_Phase"
    1.27 -  *)
    1.28 +(*~~$ ./bin/isabelle build -v -b Specify_Phase
    1.29 + *)
    1.30  session "Specify_Phase" in "Specify_Phase" = HOL +
    1.31    options [document = pdf, document_output = "output"]
    1.32    sessions
    1.33      "Specify"
    1.34    theories
    1.35      "Specify_Phase"
    1.36 -  document_files (in "../")
    1.37 -    "isabelle.sty"
    1.38 -    "isabellesym.sty"
    1.39 -    "pdfsetup.sty"
    1.40    document_files
    1.41      "root.bib"
    1.42      "root.tex"
    1.43 +    "user-requirements.tex"

     2.1 --- a/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Tue Apr 13 13:20:05 2021 +0200
     2.2 +++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Tue Apr 13 14:07:17 2021 +0200
     2.3 @@ -6,7 +6,9 @@
     2.4  (*>*)
     2.5  
     2.6  text \<open>
     2.7 -chapter \<open>Interactive Specification in an \isac-Calculation\<close>
     2.8 +\chapter{Interactive Specification in an \isac-Calculation}
     2.9 +
    2.10 +TODO
    2.11  \<close>
    2.12  
    2.13  (*<*)

     3.1 --- a/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Tue Apr 13 13:20:05 2021 +0200
     3.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Tue Apr 13 14:07:17 2021 +0200
     3.3 @@ -24,15 +24,16 @@
     3.4  \author{Walther Neuper}
     3.5  %\institute{Johannes Kepler University, Linz, Austria}
     3.6  \maketitle
     3.7 -\vspace{2cm}
     3.8  \tableofcontents
     3.9  \newpage
    3.10  
    3.11  % sane default for proof documents
    3.12  \parindent 0pt\parskip 0.5ex
    3.13  
    3.14 +\nocite{*}  %FIXME satisfy bibtex without actual text + citations
    3.15 +\input{user-requirements.tex}
    3.16 +
    3.17  % generated text of all theories
    3.18 -\input{user-requirements.tex}
    3.19  \input{Specify_Phase.tex}  %*.tex created by isabelle build
    3.20  
    3.21  % optional bibliography

     4.1 --- a/src/Tools/isac/ROOT	Tue Apr 13 13:20:05 2021 +0200
     4.2 +++ b/src/Tools/isac/ROOT	Tue Apr 13 14:07:17 2021 +0200
     4.3 @@ -56,18 +56,3 @@
     4.4      "BridgeJEdit/BridgeJEdit"
     4.5      "Knowledge/Build_Thydata"
     4.6      "Build_Isac"
     4.7 -
     4.8 -(*~~$ ./bin/isabelle build -v -b Doc          #check ok, no output
     4.9 -  *)
    4.10 -session Doc in Doc = Interpret +
    4.11 -  description "
    4.12 -    Formally checked documentation for Isac in analogy to ~~/Doc/.
    4.13 -  "
    4.14 -  options [document = false (*, browser_info = true*)]
    4.15 -  directories
    4.16 -    "Lucas_Interpreter"
    4.17 -    "Specify_Phase"
    4.18 -  theories
    4.19 -    "Lucas_Interpreter/Lucas_Interpreter"
    4.20 -    "Specify_Phase/Specify_Phase"
    4.21 -