1.1 --- a/.hgignore	Sat Dec 30 07:07:58 2023 +0100
     1.2 +++ b/.hgignore	Sat Dec 30 16:49:50 2023 +0100
     1.3 @@ -11,6 +11,9 @@
     1.4  
     1.5  syntax: regexp
     1.6  
     1.7 +src/Tools/isac/Doc/Lucas_Interpreter/output/
     1.8 +src/Tools/isac/Doc/Specify_Phase/output/
     1.9 +
    1.10  # students used various LaTeX tools (and created a mess) ------\
    1.11  ^doc-isac/.*\.aux
    1.12  ^doc-isac/.*\.bbl

     2.1 --- a/src/Tools/isac/Doc/README	Sat Dec 30 07:07:58 2023 +0100
     2.2 +++ b/src/Tools/isac/Doc/README	Sat Dec 30 16:49:50 2023 +0100
     2.3 @@ -1,7 +1,13 @@
     2.4  ~~/src/Tools/isac/Doc/README
     2.5  
     2.6  pdflatex in ~~/src/Tools/isac/Doc/ by:
     2.7 -/usr/local/isabisac/bin/isabelle build -D .
     2.8 - 
     2.9 +  ~/repos/isabisac/bin/isabelle build -D .
    2.10 +
    2.11 +.. ATTENTION: USE ONLY IN ../Doc/
    2.12 +  E.G. in isa/ CAUSES Isabelle build from scratch .. Running HOL-Mirabelle-ex
    2.13 +    + FOL, FOL-ex, .. (takes MANY min.)
    2.14 +  to ~/.isabelle/isabisac/heaps/polyml-5.9_x86_64_32-linux$
    2.15 +
    2.16 +                            
    2.17  In case nothing happens with the above command, go
    2.18 -~/.isabelle/isabisac/heaps/polyml-5.8_x86_64_32-linux/log$ rm Interpret*
    2.19 +  ~/.isabelle/isabisac/heaps/polyml-5.8_x86_64_32-linux/log$ rm Interpret*

     3.1 --- a/src/Tools/isac/Doc/ROOT	Sat Dec 30 07:07:58 2023 +0100
     3.2 +++ b/src/Tools/isac/Doc/ROOT	Sat Dec 30 16:49:50 2023 +0100
     3.3 @@ -24,4 +24,4 @@
     3.4    document_files
     3.5      "root.bib"
     3.6      "root.tex"
     3.7 -    "user-requirements.tex"
     3.8 +

     4.1 --- a/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Sat Dec 30 07:07:58 2023 +0100
     4.2 +++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Sat Dec 30 16:49:50 2023 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  (*<*)
     4.5  (*%:wrap=soft:maxLineLen=78:*)
     4.6  theory Specify_Phase
     4.7 -  imports "$ISABELLE_ISAC/Specify.Specify"
     4.8 +  imports "Specify.Specify"
     4.9  begin
    4.10  (*>*)
    4.11  

     5.1 --- a/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Sat Dec 30 07:07:58 2023 +0100
     5.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Sat Dec 30 16:49:50 2023 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -\documentclass{report}
     5.5 +\documentclass{report}
     5.6  \usepackage{isabelle,isabellesym}
     5.7  \usepackage{graphicx}
     5.8  \usepackage{paralist}  % compactitem
     5.9 @@ -31,7 +31,6 @@
    5.10  \parindent 0pt\parskip 0.5ex
    5.11  
    5.12  \nocite{*}  %FIXME satisfy bibtex without actual text + citations
    5.13 -\input{user-requirements.tex}
    5.14  
    5.15  % generated text of all theories
    5.16  \input{Specify_Phase.tex}  %*.tex created by isabelle build

     6.1 --- a/src/Tools/isac/Doc/Specify_Phase/document/user-requirements.tex	Sat Dec 30 07:07:58 2023 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,366 +0,0 @@
     6.4 -%:wrap=soft:maxLineLen=78:
     6.5 -
     6.6 -\chapter{Preliminaries}
     6.7 -%############################################################################
     6.8 -
     6.9 -\section{List of terms used in the \isac-project}\label{terms}
    6.10 -%============================================================================
    6.11 -This list follows the original one in \cite[Appendix D]{isac:all}. It is a 
    6.12 -selection concerning the specify-phase. In particular, the terms used for this 
    6.13 -phase underwent a considerable development since 2002 and are updated to the 
    6.14 -current, more convenient notions.
    6.15 -
    6.16 -\begin{description}
    6.17 -\item{\bf Calculation} is the document for interactive construction of a 
    6.18 -result from given items according to some \see Problem definition. It is a 
    6.19 -variant of ``structured derivations''~\cite{Back-SD09}.
    6.20 -
    6.21 -\item{\bf Descriptor} is the heading constant of a \see Model-Item in the 
    6.22 -fields "Given", "Find" and "Relate" (and not in where_-conditions). It indicates 
    6.23 -the kind of item and constrains the respective type.
    6.24 -
    6.25 -\item{\bf Example} specifies a particular \see Calculation. It comprises text 
    6.26 -and/or figure for the student and a \see Formalisation.
    6.27 -
    6.28 -\item{\bf Formalisation} is the formal part of an \see Example and contains 
    6.29 -data to complete a \see Specification as a prerequisite for automated 
    6.30 -generation of user-guidance in a \see Calculation.
    6.31 -
    6.32 -\item{\bf \sisac-Knowledge} comprises collections of three kinds of knowledge:
    6.33 -  \begin{compactitem}
    6.34 -  \item {\bf RTheory}, an Isabelle theory
    6.35 -  \item {\bf RProblem} is a \see Model-Pattern.
    6.36 -  \item {\bf RMethod}: a program guarded by a \see Model serving 
    6.37 -    ``Lucas-Interpre-tation''~\cite{EPTCS-wn-20}.
    6.38 -  \end{compactitem}
    6.39 -  For simplicity reasons, a collection of \see Examples is subsumed to  
    6.40 -    \sisac-Knowledge, too.
    6.41 -
    6.42 -\item{\bf Method} is a program for a class of Problems. It consists of a   
    6.43 -program to be exploited by Lucas-Interpretation \cite{EPTCS-wn-20} and a guard   
    6.44 -with the structure of a \see Model.
    6.45 -
    6.46 -\item{\bf Model} comprises four fields of \see Model-Items in the line  
    6.47 -of~\cite{gries}:
    6.48 -  \begin{compactitem}
    6.49 -  \item {\bf Given} for the input-items
    6.50 -  \item {\bf Where} for the where_-conditions constraining the input-items
    6.51 -  \item {\bf Find} for the output-items
    6.52 -  \item {\bf Relate} for a part of the post-condition capturing the essence of 
    6.53 -    a problem relating input and output
    6.54 -  \end{compactitem}
    6.55 -
    6.56 -\item{\bf Model-Item} is a mathematical term in a \see Model.
    6.57 -
    6.58 -\item{\bf Model-Pattern} comprises the same fields as a \see Model, but these 
    6.59 -contain variables to be instanted by the \see Formalisation of an \see Example 
    6.60 -in order to give \see Model.
    6.61 -
    6.62 -\item{\bf Problem} is the head of a \see Calculation. Calculations can 
    6.63 -comprise several sub-problems, arbitrarily nested, with exactly the same 
    6.64 -structure. A Problem consists of a \see Specification and a \see Solution.
    6.65 -
    6.66 -\item{\bf References} refer to three kinds of items in the \see 
    6.67 -\sisac-Knowledge.
    6.68 -
    6.69 -\item{\bf Solution} are the steps form a \see Specification to a \see 
    6.70 -Solution, where each step is justified by a \see Tactic. The final step 
    6.71 -fulfills the post-condition of the \see Model.
    6.72 -
    6.73 -\item{\bf Specification} comprises data to specify a problem in the \see Model 
    6.74 -and gives \see References into the \see \sisac-Knowledge.
    6.75 -
    6.76 -\item{\bf Tactic} transforms a term into another, frequently a rewrite-rule. 
    6.77 -Since a \see Problem can occur recusively in a Solution as a sub-problem, this 
    6.78 -is also a particular Tactic.
    6.79 -
    6.80 -\item{\bf User-Guide} supports a student during interactive \see Calculations. 
    6.81 -This support is only possible if a \see Formalisation has been transferred 
    6.82 -(invisibly for a student) from an \see Example.
    6.83 -
    6.84 -%\item{\bf TODO} xxx
    6.85 -\end{description}
    6.86 -
    6.87 -
    6.88 -\section{User Requirements}
    6.89 -%============================================================================
    6.90 -The User Requirements ({\bf UR}s) do not follow the lines of the original ones 
    6.91 -in \cite[Part I]{isac:all}, but limit themselves to a student in the 
    6.92 -specify-phase and use the updated terms from \S\ref{terms} (which are 
    6.93 -indicated by initial capital letters).
    6.94 -
    6.95 -\subsection{General}
    6.96 -%----------------------------------------------------------------------------
    6.97 -{\bf\UR{The screen-reader superimposes the Braille display \label{sreader-braille}}} in the software hierarchy, i.e. the former determines output of the latter.
    6.98 -
    6.99 -{\bf\UR{Special keys can be defined by the user\label{def-spec-keys}}} for the Braille display.
   6.100 -
   6.101 -\subsection{Specify Phase}
   6.102 -%----------------------------------------------------------------------------
   6.103 -{\bf\UR{Examples are selected from 
   6.104 -collections\label{example-coll}}}\footnote{The present test setup bypasses 
   6.105 -this UR.}
   6.106 -implemented on web-pages, which look like a text book. A specific link at an 
   6.107 -Example starts an interactive Calculation for that Example. See 
   6.108 -\url{http://www.ist.tugraz.at/projects/isac/www/kbase/exp/exp_Statics_Biegel_Timischl.html}.
   6.109 -
   6.110 -{\bf\UR{A Calculation is headed by the keyword Problem\label{yyy}}} and in 
   6.111 -case of standard problems from Computer Algebra with a respective command like 
   6.112 -${\it simplify} (x + 1 + 2)$ or ${\it solve} (x + 1 = 2, \,x)$. An example is 
   6.113 -Expl.\ref{tab:ca}. A Calculation can have sub-Problems with exactly the same 
   6.114 -structure.
   6.115 -
   6.116 -{\bf\UR{A Calculation can be completed with one keystroke\label{yyy}}} and 
   6.117 -sub-Problems as well, when allowed by the User-Guide. See 
   6.118 -Expl.\ref{tab:calc-coll}.
   6.119 -
   6.120 -{\bf\UR{Switching between survey and detail\label{yyy}}} is supported by 
   6.121 -collapsing and expanding a Calculation, see Expl.\ref{tab:calc-exp} \dots 
   6.122 -Expl.\ref{tab:model-sub}
   6.123 -
   6.124 -{\bf\UR{A Calculation can be started from scratch\label{yyy}}}, that means 
   6.125 -without a preceding Example. In this case an empty Specification is generated 
   6.126 -by the system (see Expl.\ref{tab:mod-empty}) and the User-Guide cannot help 
   6.127 -the student completing the Specification.
   6.128 -
   6.129 -{\bf\UR{Input to the Model is guided by Descriptors\label{yyy}}}, see 
   6.130 -Expl.\ref{tab:model}, which are given by the Model-Pattern for the specific 
   6.131 -kind of Problem.
   6.132 -
   6.133 -{\bf\UR{Feedback during input to the Model\label{yyy}}} is given as
   6.134 -\begin{compactitem}
   6.135 -\item ``correct''
   6.136 -\item ``syntax-error'' or type error
   6.137 -\item ``superfluous''
   6.138 -\item ``incomplete'' in case of lists, sets, etc.
   6.139 -\item ``missing''
   6.140 -\item ``true'' or ``false'' for predicates in the field Where.
   6.141 -\end{compactitem}
   6.142 -
   6.143 -{\bf\UR{Feedback during input to References\label{yyy}}} is given in the 
   6.144 -Model:
   6.145 -\begin{compactitem}
   6.146 -\item Update RTheory: might cause ``syntax-error''
   6.147 -\item Update RProblem: might cause ``superfluous'' or ``missing''
   6.148 -\item Update RMethod: in this case the Model shows the guard with 
   6.149 -``superfluous'' or ``missing'' and the keyword Model is annotated with 
   6.150 -``(RMethod)''.
   6.151 -\end{compactitem}
   6.152 -
   6.153 -{\bf\UR{The Model can be switched between RProblem and RMethod,\label{yyy}}} 
   6.154 -where the latter is indicated by ``Model (RMethod)''< see Expl.\ref{tab:refs}.
   6.155 -
   6.156 -\subsection{Terms}
   6.157 -%----------------------------------------------------------------------------
   6.158 -{\bf\UR{Terms are presented as strings in Braille format\label{term-str}}} for 
   6.159 -the blind user and as Isabelle strings for other users at the same time --- 
   6.160 -for the purpose of inclusive learning in front of one and the same screen. 
   6.161 -?TODO is this reasonable?
   6.162 -
   6.163 -{\bf\UR{The Braille-format can be changed\label{braille-format}}} to different 
   6.164 -standards.
   6.165 -
   6.166 -{\bf\UR{Braille-format can be displayed also in the standard frontend\label{braille-format-standard}}}, in particular for authoring purposes.
   6.167 -
   6.168 -{\bf\UR{Semantic information is available for all elements of 
   6.169 -terms.\label{term-semantic}}} Such information is:
   6.170 -\begin{compactenum}
   6.171 -\item the type for constants and variables by a pop-up.
   6.172 -\item the scope of a variable by (TODO ``internal'' and ``global'' seems to 
   6.173 -coarse).
   6.174 -\item the definition of constants and variables by jumping to the respective 
   6.175 -location, probably in another file.
   6.176 -\end{compactenum}
   6.177 -
   6.178 -{\bf\UR{On the Braille lines of pop-ups start with a special character\label{indicate-popup}}}, TODO? ``\#''.
   6.179 -
   6.180 -{\bf\UR{Sub-terms are presented as strings\label{sub-term-str}}} the same way 
   6.181 -as whole terms. ?TODO? show location within the whole term.
   6.182 -
   6.183 -{\bf\UR{A term can be shown as a tree\label{term-tree}}} if requested by a 
   6.184 -special key, TODO SK1. The key followed by an integer argument determines the 
   6.185 -depth of the tree. For instance $<$SK1 2$>$ displays the term 
   6.186 -$\frac{\frac{1}{x+2*y}}{\frac{3}{z}}$ 
   6.187 -\begin{tabbing}
   6.188 -123\=\#3.2 \=$/$ \=$/$ \=    \kill
   6.189 -   \>\#    \>$/$     \\
   6.190 -   \>\#1   \>\>$/$     \\
   6.191 -   \>\#1.1 \>\>\> 1    \\
   6.192 -   \>\#1.2 \>\>\> x + 2 * y\\
   6.193 -   \>\#2.  \>\>$/$     \\
   6.194 -   \>\#2.1 \>\>\> 3    \\
   6.195 -   \>\#2.2 \>\>\> z
   6.196 -\end{tabbing}
   6.197 -Note that there are operators with different arity, for instance arity one for $\sin$, arity two for $+$ and arity four for $\int^a_b\;f(x)\;dx{}$.
   6.198 -
   6.199 -{\bf\UR{Structure of the tree representation\label{yyy}}} of a term is (?TODO\dots) indicated by integer lists as shown in the example of UR\ref{term-tree}.
   6.200 -
   6.201 -{\bf\UR{Collapsing and expanding of the tree representation \label{term-coll-exp}}} for a term follow the rules established for file browsers.
   6.202 -
   6.203 -{\bf\UR{Special keys lead to the node at the deepest level\label{yyy}}} and ?TODO?
   6.204 -
   6.205 -{\bf\UR{Navigation through sub-terms is hierarchical\label{navi-sub-terms}}} 
   6.206 -and supported by a special key combined with the arrow keys as follows:
   6.207 -\begin{compactenum}
   6.208 -\item $<$STRG$>$ $<\rightarrow>$ next element right on the same level; 
   6.209 -acoustical indication at the end of the level.
   6.210 -\item $<$STRG$>$ $<\leftarrow>$ next element left on the same level; 
   6.211 -acoustical indication at the end of the level.
   6.212 -\item $<$STRG$>$ $<\uparrow>$ next element on the higher level; acoustical 
   6.213 -indication at the root.
   6.214 -\item $<$STRG$>$ $<\downarrow>$ next element on the lower level; acoustical 
   6.215 -indication at the bottom.
   6.216 -\end{compactenum}
   6.217 -
   6.218 -%{\bf\UR{xxx.\label{yyy}}}
   6.219 -
   6.220 -
   6.221 -\section{Example Calculations}
   6.222 -%============================================================================
   6.223 -Calculations at different stages of interactive steps towards a Solution and 
   6.224 -with variants of collapsing and expanding.\\
   6.225 -
   6.226 -{\bf\Expl{Complete Calculation expanded (sub-Problems 
   6.227 -collapsed).\label{tab:calc-exp}}}
   6.228 -{\tiny \begin{tabbing}
   6.229 -12\=12\=12\=12\=\kill
   6.230 -Example $<$7.70 a$>$              \\
   6.231 -Problem ("Biegelinie", \dots)     \\
   6.232 -.\>Specification:                 \\
   6.233 -.\>.\>Model:                      \\
   6.234 -.\>.\>.\>Given: "Traeger L",      \\
   6.235 -.\>.\>.\>Where: "q\_0 ist\dots    \\
   6.236 -.\>.\>.\>Find: "Biegelinie y"     \\
   6.237 -.\>.\>.\>Relate: "Rand\dots       \\
   6.238 -.\>.\>References:                 \\
   6.239 -.\>.\>.\>RTheory: "Bie\dots"      \\
   6.240 -.\>.\>.\>RProblem: ["\dots]       \\
   6.241 -.\>.\>.\>RMethod: ["Int\dots]     \\
   6.242 -.\>Solution:                      \\
   6.243 -.\>.\>Problem ("\dots")           \\
   6.244 -.\>.\>"[Q x = c + -1 * \dots"     \\
   6.245 -.\>\vdots                         \\
   6.246 -.\>."y x = $-6 * q\_0 * *$\dots"  \\
   6.247 -"y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
   6.248 -\end{tabbing}}
   6.249 -
   6.250 -{\bf\Expl{Complete Calculation collapsed.\label{tab:calc-coll}}}
   6.251 -{\tiny \begin{tabbing}
   6.252 -12\=12\=12\=12\=\kill
   6.253 -Example $<$7.70 a$>$              \\
   6.254 -Problem ("Biegelinie", \dots)     \\
   6.255 -"y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
   6.256 -\end{tabbing}}
   6.257 -
   6.258 -\newpage %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   6.259 -{\bf\Expl{Interactive Specification editing the Model\label{tab:model}}}, the 
   6.260 -inital state with Descriptors, if given by the Example:
   6.261 -{\tiny \begin{tabbing}
   6.262 -12\=12\=12\=12\=\kill
   6.263 -Example $<$7.70 a$>$                        \\
   6.264 -Problem ("Biegelinie", \dots)               \\
   6.265 -.\>Specification:                           \\
   6.266 -.\>.\>Model:                                \\
   6.267 -.\>.\>.\>Given: "Traeger ", "Streckenlast " \\
   6.268 -.\>.\>.\>Where:                             \\
   6.269 -.\>.\>.\>Find: "Biegelinie "                \\
   6.270 -.\>.\>.\>Relate: "Randbedingungen [ ]"      \\
   6.271 -.\>.\>References:                           \\
   6.272 -.\>Solution:
   6.273 -\end{tabbing}}
   6.274 -
   6.275 -{\bf\Expl{Interactive Specification from scratch\label{tab:mod-empty}}}, the 
   6.276 -system presents an empty Specification:
   6.277 -{\tiny \begin{tabbing}
   6.278 -12\=12\=12\=12\=\kill
   6.279 -Problem ("", [])            \\
   6.280 -.\>Specification:           \\
   6.281 -.\>.\>Model:                \\
   6.282 -.\>.\>.\>Given: "", ""      \\
   6.283 -.\>.\>.\>Where: "", ""      \\
   6.284 -.\>.\>.\>Find:  ""          \\
   6.285 -.\>.\>.\>Relate: "", ""     \\
   6.286 -.\>.\>References:           \\
   6.287 -.\>.\>.\>RTheory: ""        \\
   6.288 -.\>.\>.\>RProblem: ["", ""] \\
   6.289 -.\>.\>.\>RMethod: ["", ""]  \\
   6.290 -.\>Solution:
   6.291 -\end{tabbing}}
   6.292 -
   6.293 -{\bf\Expl{Interactive Specification editing References\label{tab:refs}}}, here 
   6.294 -shown for RTheory and for RProblem; such editing is usually done after some 
   6.295 -input to the Model:
   6.296 -{\tiny \begin{tabbing}
   6.297 -12\=12\=12\=12\=\kill
   6.298 -Example $<$7.70 a$>$                        \\
   6.299 -Problem ("Biegelinie", \dots)               \\
   6.300 -.\>Specification:                           \\
   6.301 -.\>.\>Model:                                \\
   6.302 -.\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$"                 \\
   6.303 -.\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
   6.304 -.\>.\>.\>Find: "Biegelinie y"               \\
   6.305 -.\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x 
   6.306 -                    y_0 = 0 ]$"             \\
   6.307 -.\>.\>References:                           \\
   6.308 -.\>.\>.\>RTheory: {\bf"Biegelinie"}         \\
   6.309 -.\>.\>.\>RProblem: ["Biegelinien"]          \\
   6.310 -.\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"]             \\
   6.311 -.\>Solution:
   6.312 -\end{tabbing}}
   6.313 -
   6.314 -{\bf\Expl{Interactive Specification editing RMethod\label{tab:refs-met}}}. The 
   6.315 -additional Given item "FunktionsVariable $x$" is usually provided behind the 
   6.316 -scenes; but in case of editing RMethod the "Model (RMethod)" is shown and can 
   6.317 -be edited as well.
   6.318 -{\tiny \begin{tabbing}
   6.319 -12\=12\=12\=12\=\kill
   6.320 -Example $<$7.70 a$>$                        \\
   6.321 -Problem ("Biegelinie", \dots)               \\
   6.322 -.\>Specification:                           \\
   6.323 -.\>.\>Model (RMethod):                      \\
   6.324 -.\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$", "FunktionsVariable 
   6.325 -                   $x$" \\
   6.326 -.\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
   6.327 -.\>.\>.\>Find: "Biegelinie y"               \\
   6.328 -.\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x 
   6.329 -                    y_0 = 0 ]$"             \\
   6.330 -.\>.\>References:                           \\
   6.331 -.\>.\>.\>RTheory: {\bf"Biegelinie"}         \\
   6.332 -.\>.\>.\>RProblem: ["Biegelinien"]          \\
   6.333 -.\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"]             \\
   6.334 -.\>Solution:
   6.335 -\end{tabbing}}
   6.336 -
   6.337 -{\bf\Expl{Interactively solving the sub-Problem.\label{tab:model-sub}}}
   6.338 -{\tiny \begin{tabbing}
   6.339 -12\=12\=12\=12\=12\=\kill
   6.340 -Example $<$7.70 a$>$             \\
   6.341 -Problem ("Biegelinie", \dots)    \\
   6.342 -.\>Specification:                \\
   6.343 -.\>Solution:                     \\
   6.344 -.\>.\>Problem ("\dots")          \\
   6.345 -.\>.\>.\>Specification:          \\
   6.346 -.\>.\>.\>.\>Model:               \\
   6.347 -.\>.\>.\>.\>.\>Given: "\dots"    \\
   6.348 -.\>.\>.\>.\>.\>Where: "\dots"    \\
   6.349 -.\>.\>.\>.\>.\>Find: "\dots"     \\
   6.350 -.\>.\>.\>.\>.\>Relate: "\dots    \\
   6.351 -.\>.\>.\>.\>References:          \\
   6.352 -.\>.\>.\>Solution:               \\
   6.353 -\end{tabbing}}
   6.354 -
   6.355 -{\bf\Expl{Calculation like in Computer Algebra.\label{tab:ca}}}
   6.356 -{\tiny \begin{tabbing}
   6.357 -12\=12\=12\=12\=\kill
   6.358 -Example $<$123 d$>$             \\
   6.359 -${\it solve} (x + 1 = 2, \,x)$  \\
   6.360 -.\>Specification:               \\
   6.361 -.\>Solution:                    \\
   6.362 -.\>.\>"$x + 1 = 2$"             \\
   6.363 -.\>.\>"$x = 2 - 1$"             \\
   6.364 -.\>.\>"$x = 1$"                 \\
   6.365 -"$x = 1$"
   6.366 -\end{tabbing}}
   6.367 -
   6.368 -%\subsection{TODO}
   6.369 -%\subsubsection{TODO}

     7.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Dec 30 07:07:58 2023 +0100
     7.2 +++ b/test/Tools/isac/Test_Isac.thy	Sat Dec 30 16:49:50 2023 +0100
     7.3 @@ -83,6 +83,9 @@
     7.4  (*Test_Isac.thy*)
     7.5    "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
     7.6  
     7.7 +  "$ISABELLE_ISAC/Doc/Lucas_Interpreter/Lucas_Interpreter"                    (*Test_Isac_Short*)
     7.8 +  "$ISABELLE_ISAC/Doc/Specify_Phase/Specify_Phase"                            (*Test_Isac_Short*)
     7.9 +
    7.10  begin
    7.11  
    7.12  declare [[ML_print_depth = 20]] (*otherwise buffer overflow*)

     8.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Sat Dec 30 07:07:58 2023 +0100
     8.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sat Dec 30 16:49:50 2023 +0100
     8.3 @@ -83,6 +83,9 @@
     8.4  ( *Test_Isac_Short.thy*)
     8.5    "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
     8.6  
     8.7 +(*"$ISABELLE_ISAC/Doc/Lucas_Interpreter/Lucas_Interpreter"                    Test_Isac_Short*)
     8.8 +(*"$ISABELLE_ISAC/Doc/Specify_Phase/Specify_Phase"                            Test_Isac_Short*)
     8.9 +
    8.10  begin
    8.11  
    8.12  declare [[ML_print_depth = 20]] (*otherwise buffer overflow*)