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

     2.1 --- a/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Thu Apr 08 13:27:27 2021 +0200
     2.2 +++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Tue Apr 13 13:20:05 2021 +0200
     2.3 @@ -5,6 +5,9 @@
     2.4  begin
     2.5  (*>*)
     2.6  
     2.7 +text \<open>
     2.8 +chapter \<open>Interactive Specification in an \isac-Calculation\<close>
     2.9 +\<close>
    2.10  
    2.11  (*<*)
    2.12  end

     3.1 --- a/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Thu Apr 08 13:27:27 2021 +0200
     3.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Tue Apr 13 13:20:05 2021 +0200
     3.3 @@ -1,6 +1,7 @@
     3.4 -\documentclass{article}
     3.5 +\documentclass{report}
     3.6  \usepackage{isabelle,isabellesym}
     3.7  \usepackage{graphicx}
     3.8 +\usepackage{paralist}  % compactitem
     3.9  % this should be the last package used
    3.10  \usepackage{pdfsetup}
    3.11  
    3.12 @@ -13,6 +14,9 @@
    3.13  
    3.14  \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    3.15  \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    3.16 +\def\see{$\rightarrow$}
    3.17 +\newtheorem{UR}{UR}[section]
    3.18 +\newtheorem{Expl}{Expl}[section]
    3.19  
    3.20  \begin{document}
    3.21  
    3.22 @@ -27,10 +31,8 @@
    3.23  % sane default for proof documents
    3.24  \parindent 0pt\parskip 0.5ex
    3.25  
    3.26 -\nocite{*}  %FIXME satisfy bibtex without actual text + citations
    3.27 -%\input{user-requirements.tex}  %FIXME does not quite work yet
    3.28 -
    3.29  % generated text of all theories
    3.30 +\input{user-requirements.tex}
    3.31  \input{Specify_Phase.tex}  %*.tex created by isabelle build
    3.32  
    3.33  % optional bibliography

     4.1 --- a/src/Tools/isac/Doc/Specify_Phase/document/user-requirements.tex	Thu Apr 08 13:27:27 2021 +0200
     4.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/user-requirements.tex	Tue Apr 13 13:20:05 2021 +0200
     4.3 @@ -1,20 +1,4 @@
     4.4  %:wrap=soft:maxLineLen=78:
     4.5 -%remove after isabelle build started working -----------------
     4.6 -\documentclass{article}
     4.7 -\usepackage{../../isabelle,../../isabellesym}
     4.8 -\usepackage{graphicx}
     4.9 -
    4.10 -\usepackage{hyperref}  %\url{...}  don't use together with isabelle
    4.11 -\usepackage{breakurl}  %\url{...}  don't use together with isabelle
    4.12 -\usepackage{paralist}  % compactitem
    4.13 -
    4.14 -\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    4.15 -\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    4.16 -\def\see{$\rightarrow$}
    4.17 -\newtheorem{UR}{UR}[section]
    4.18 -\newtheorem{Expl}{Expl}[section]
    4.19 -
    4.20 -\begin{document}
    4.21  
    4.22  \section{List of terms used in the \isac-project}\label{terms}
    4.23  %============================================================================
    4.24 @@ -305,12 +289,5 @@
    4.25  "$x = 1$"
    4.26  \end{tabbing}}
    4.27  
    4.28 -
    4.29 -
    4.30  %\subsection{TODO}
    4.31  %\subsubsection{TODO}
    4.32 -
    4.33 -\bibliographystyle{plain}
    4.34 -\bibliography{root}
    4.35 -
    4.36 -\end{document}

     5.1 --- a/src/Tools/isac/ROOT	Thu Apr 08 13:27:27 2021 +0200
     5.2 +++ b/src/Tools/isac/ROOT	Tue Apr 13 13:20:05 2021 +0200
     5.3 @@ -56,3 +56,18 @@
     5.4      "BridgeJEdit/BridgeJEdit"
     5.5      "Knowledge/Build_Thydata"
     5.6      "Build_Isac"
     5.7 +
     5.8 +(*~~$ ./bin/isabelle build -v -b Doc          #check ok, no output
     5.9 +  *)
    5.10 +session Doc in Doc = Interpret +
    5.11 +  description "
    5.12 +    Formally checked documentation for Isac in analogy to ~~/Doc/.
    5.13 +  "
    5.14 +  options [document = false (*, browser_info = true*)]
    5.15 +  directories
    5.16 +    "Lucas_Interpreter"
    5.17 +    "Specify_Phase"
    5.18 +  theories
    5.19 +    "Lucas_Interpreter/Lucas_Interpreter"
    5.20 +    "Specify_Phase/Specify_Phase"
    5.21 +