# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1583936752 -3600
# Node ID 168abe8dd1e39fd5775b04f70bbb3d3e46961bb6
# Parent  fac2f374d001f890ed7dd1b74548ebd136921e43
start formally checked documentation with Lucas_Interpreter

note: the text is a partial copy from the IJCAR/ThEdu'20 paper

diff -r fac2f374d001 -r 168abe8dd1e3 doc-isac/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-isac/README	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,7 @@
+~~/doc-isac/README
+
+Much documentation is still in theses are found at
+https://isac.miraheze.org/wiki/Publications_and_Theses#Refereed_Papers
+
+In March 2020 formally checked documentation started in
+~~/src/Tools/isac/Doc
\ No newline at end of file
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/CLEANUP
--- a/src/Tools/isac/CLEANUP	Tue Mar 10 13:25:00 2020 +0100
+++ b/src/Tools/isac/CLEANUP	Wed Mar 11 15:25:52 2020 +0100
@@ -57,6 +57,19 @@
   rm *.orig~~
   rm *.orig~~~
   cd .. 
+cd Doc
+  rm *~
+  cd Lucas_Interpreter
+    rm *~
+    cd document
+      rm *~
+      cd ..
+    cd output
+      rm *
+      rm -rf document/
+      cd ..
+    cd ..
+  cd ..
 cd ProgLang
   echo "cd ProgLang was successful -------------------------------------------------------------"
   rm *.sml~
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,615 @@
+(*<*)
+(*%:wrap=soft:maxLineLen=78:*)
+(*partially copied from
+  ~/material/texts/emat/lucin-isa/paper-isabisac/Lucin_Isa_IJCAR.thy *)
+theory Lucas_Interpreter
+  imports "~~/src/Tools/isac/Interpret/Interpret"
+begin
+ML \<open>
+  open LI
+  open Istate
+  open TermC
+\<close>
+(*>*)
+
+text \<open>
+\section{Lucas--Interpretation (\LI)}\label{lucin}
+%=============================================================================
+The interpreter is named after the inventor of top-down-parsing in the ALGOL 
+project~\cite{pl:formal-lang-hist}, Peter Lucas. As a dedicated expert in 
+programming languages he initially objected ``yet another programming 
+language'' (in analogy to ``Yacc'' \cite{Yacc-1975}), but then he helped to 
+clarify the unusual requirements for a novel programming language in the 
+\sisac-project, which later led to the notion of \LI. 
+
+\LI{} is the most prominent component in a prototype developed in the 
+\sisac-project, there embedded in a mathematics-engine, which interacts with a 
+dialogue-module in a Java-based front-end managing interaction with students 
+(out of scope of this paper).
+
+\subsection{The Concept of \LI}\label{concept-LI}
+%-----------------------------------------------------------------------------
+The concept of \LI{} is simple: \LI{} \emph{acts as a debugger on functional 
+programs with hard-coded breakpoints, where control is handed over to a 
+student; a student, however, does \emph{not} interact with the software 
+presenting the program, but with the software presenting steps of forward 
+reasoning, where the steps are rigorously constructed by tactics acting as the 
+break-points mentioned}. Following the \LI{} terminology, we will call 
+``programs'' the functions defined with the function package and refer to 
+their evaluation as ``execution''.
+
+\paragraph{Types occurring in the signatures} of \LI{} are as follows. Besides 
+the program of type @{ML_type Program.T} there is an interpreter state 
+@{ML_type Istate.T}, a record type passing data from one step of execution to 
+the next step, in particular a location in the program, where the next step 
+will be read off, and an environment for evaluating the step.
+As invisible in the program language as the interpreter state is @{ML_type 
+Calc.T}, a ``calculation'' as a sequence of steps in forward reasoning, a 
+variant of ``structured derivations'' \cite{back-SD-2010}. Visible in the 
+language and in the signature, however, are the tactics @{ML_type Tactic.T}, 
+which create steps in a calculation.
+
+Novel in connection with calculations is the idea to maintain a logical 
+context in order to provide automated provers with data required for checking 
+input by the student. Isabelle's @{ML_type Proof.context}, as is, turned out 
+perfect for this task~\cite{mlehnf:bakk-11}.
+
+\paragraph{The signatures of the main functions,} the functions @{term 
+find_next_step}, \\@{term locate_input_tactic} and @{term locate_input_term}, 
+are as follows:\label{sig-lucin}
+\<close>
+(*<*)ML(*>*) \<open>
+signature LUCAS_INTERPRETER =
+sig
+  datatype next_step_result =
+      Next_Step of Istate.T * Proof.context * Tactic.T
+    | Helpless | End_Program of Istate.T * Tactic.T
+  val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context
+    -> next_step_result
+
+  datatype input_tactic_result =
+      Safe_Step of Istate.T * Proof.context * Tactic.T
+    | Unsafe_Step of Istate.T * Proof.context * Tactic.T
+    | Not_Locatable of message
+  val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context
+      -> Tactic.T -> input_tactic_result
+
+  datatype input_term_result =
+    Found_Step of Calc.T | Not_Derivable
+  val locate_input_term: Calc.T -> term -> input_term_result
+end
+\<close>
+text \<open>
+\begin{description}
+\item[@{term find_next_step}] accomplishes what usually is expected from a 
+@{ML_type Program.T}: find a @{term Next_Step} to be executed, in the case of 
+\LI{} to be inserted into a \texttt{\small Calc.T} under construction. This 
+step can be a @{ML_type Tactic.T}, directly found in @{term next_step_result}, 
+or a @{ML_type term} produced by applying the tactic. If such a step cannot be 
+found (due to previous student interaction), \LI{} is @{term Helpless}.
+
+\item[@{term locate_input_tactic}] gets a  @{ML_type Tactic.T} as argument 
+(which has been input and checked applicable in  @{ML_type  Calc.T}) and tries 
+to locate it in the \texttt{Prog.T} such that a @{term Next_Step} can be 
+generated from the subsequent location in the @{ML_type Program.T}. A step can 
+be an @{term Unsafe_Step}, if the input @{ML_type Tactic.T} cannot safely be 
+associated with any tactic in the @{ML_type Program.T}. This function has a 
+signature similar to @{term find_next_step} (here the respective input 
+@{ML_type Tactic.T} and the one in the result are the same) in order to unify 
+internal technicalities of \LI{}.
+
+\item[@{term locate_input_term}] tries to find a derivation from the current 
+@{ML_type Proof.context} for the term input to @{ML_type Calc.T} and to locate 
+a \texttt{Tactic.T} in the @{ML_type Program.T}, which as @{term Found_Step} 
+allows to find a next step later. Such a @{term Found_Step} can be located in 
+another program (a sub-program or a calling program); thus @{ML_type 
+Program.T}, @{ML_type Istate.T} and @{ML_type Proof.context} are packed into 
+@{ML_type Calc.T} at appropriate positions and do not show up in the 
+signature.
+\end{description}
+
+Automated reasoning is concern of the third function @{term 
+locate_input_term}, actually a typical application case for Isabelle's 
+Sledgehammer~\cite{sledgehammer-tutorial}, but not yet realised and 
+preliminarily substituted by \sisac's simplifier. @{term locate_input_term} is 
+the function used predominantly in interaction with students: these input term 
+by term into the calculation under construction (as familiar from 
+paper\&pencil work) and \LI{} checks for correctness automatically.
+\<close>
+text \<open>
+\subsection{Examples for \LI}\label{expl-lucin}
+%-----------------------------------------------------------------------------
+\LI's novel concept relating program execution with construction of 
+calculations is best demonstrated by examples. The first one is from 
+structural engineering given by the following problem statement:\\
+\medskip
+
+% first column
+\begin{minipage}{0.55\textwidth}
+\textit{Determine the bending line of a beam of length $L$,
+which consists of homogeneous material, which is clamped on one side
+and which is under constant line load $q_0$; see the Figure right.}\\
+\end{minipage}
+\hfill
+%second column
+\begin{minipage}{0.42\textwidth}
+  \includegraphics[width=0.6\textwidth]{bend-7-70-en.png}\\
+\end{minipage}
+
+\medskip
+This problem is solved by the following program, which is shown by a 
+screen-shot\footnote{The corresponding code is at 
+\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/Knowledge/Biegelinie.thy\#l174}.
+%When inner syntax double-quotes are discontinued eventually, the inner syntax 
+of the HOL library may use double quotes for char/string literals, instead of 
+slightly odd double single-quotes.
+}
+in order to demonstrate the colouring helpful for programmers (compare the old 
+bare string version in \cite[p.~92]{wn:proto-sys}).
+\begin{figure} [htb]
+  \centering
+  \includegraphics[width=\textwidth]{fun-pack-biegelinie-2.png}
+  \caption{The program implemented by the function package}
+  \label{fig:fun-pack-biegelinie}
+\end{figure}
+The program is implemented as a @{theory_text partial_function}: it calculates 
+results for a whole class of problems and termination cannot be proven in such 
+generality, although preconditions guard execution.
+%
+The program reflects a ``divide \& conquer'' strategy by calling three @{term 
+SubProblem}s. It was implemented for field-tests in German-speaking countries, 
+so arguments of the @{term SubProblem}s are in German, because they appear in 
+the calculation as well. The third @{term SubProblem} adopts the format from 
+Computer Algebra. The calculation, if finished successfully, looks as follows 
+(a screen-shot of intermediate steps on the prototype's front-end is shown in 
+\cite[p.~97]{wn:proto-sys}):\label{biegel_calc}
+{\footnotesize\begin{tabbing}
+123\=12\=12\=12\=12\=12\=12\=123\=123\=123\=123\=\kill
+01\> Problem (Biegelinie, [Biegelinien]) \\
+02\>\> Specification: \\
+03\>\> Solution: \\
+04\>\>\> Problem (Biegelinie, [vonBelastungZu, Biegelinien]) \\
+05\>\>\> $[$\>$V\,x = c + -1\cdot q_0\cdot x, $\\
+06\>\>\>    \>$M_b\,x = c_2 + c\cdot x + \frac{-1\cdot q_0}{2\cdot x ^ 2}, $\\
+07\>\>\>    \>$\frac{d}{dx}y\,x =  c_3 + \frac{-1}{EI} \cdot (c_2\cdot x + 
+\frac{c}{2\cdot x ^ 2} + \frac{-1\cdot q_0}{6\cdot x ^ 3}, $\\
+08\>\>\>    \>$y\,x =  c_4 + c_3\cdot x +  \frac{-1}{EI} \cdot  
+(\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot 
+q_0}{24}\cdot x ^ 4)\;\;]$ \\
+09\>\>\> Problem (Biegelinie, [setzeRandbedingungen, Biegelinien])\\
+10\>\>\> $[$\>$L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L \cdot c + 
+-1 \dot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;]$\\
+11\>\>\> solveSystem $(L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L 
+\cdot c + -1 \cdot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;],\; [c, c_2, 
+c_3, c_4])$\\
+12\>\>\> $[$\>$c = L \cdot q_0 ,\; c_2 = \frac{-1 \cdot L ^ 2 \cdot q_0}{2},\; 
+c_3 = 0,\; c_4 = 0]$\\
+13  \` Take $y\,x =  c_4 + c_3\cdot x +  \frac{-1}{EI} \cdot  
+(\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot 
+q_0}{24}\cdot x ^ 4)$ \\
+
+14\>\>\> $y\,x = c_4 + c_3 \cdot x + \frac{-1}{EI} \cdot (\frac{c_2}{2} \cdot 
+x ^ 2 + \frac{c}{6} \cdot x ^ 3 + \frac{-1 \cdot q_0}{24} \cdot x ^ 4)$\\
+15  \` Substitute $[c,c_2,c_3,c_4]$ \\
+
+16\>\>\> $y\,x = 0 + 0 \cdot x + \frac{-1}{EI} \cdot (\frac{\frac{-1 \cdot L ^ 
+2 \cdot q_0}{2}}{2} \cdot x ^ 2 + \frac{L \cdot q_0}{6} \cdot x ^ 3 + \frac{-1 
+\cdot q_0}{24} \cdot x ^ 4)$\label{exp-biegel-Substitute}\\
+17  \` Rewrite\_Set\_Inst $([({\it bdv},x)], {\it make\_ratpoly\_in})$ \\
+
+18\>\>\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L 
+\cdot q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$\\
+19\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L \cdot 
+q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$
+\end{tabbing}}
+The calculation is what a student interacts with. Above the \texttt{\small 
+Specification} is folded in, the specification phase and respective user 
+interaction is skipped here. The \texttt{\small Solution} must be constructed 
+step-wise line by line (while the line numbers do not belong to the 
+calculation) in forward reasoning. 
+\label{1-2-3}A student inputs either (1) a term (displayed on the left above 
+with indentations) or (2) a tactic (shifted to the right margin). If the 
+student gets stuck (3) a next step (as a term or a tactic) is suggested by 
+\LI{}, which works behind the scenes; the corresponding functions have been 
+introduced in \S\ref{concept-LI} (for (1) @{term locate_input_term}, (2) 
+@{term locate_input_tactic} and for (3) @{term find_next_step}).
+
+\medskip
+This example hopefully clarifies the relation between program and calculation 
+in \LI{}: execution of the program stops at tactics (above called  
+break-points), displays the tactic or the result produced by the tactic (as 
+decided by the dialogue-module) in the calculation under construction, hands 
+over control to the student working on the calculation and resumes checking 
+user input.
+
+\paragraph{A typical example from Computer Algebra}\label{expl-rewrite} shall 
+shed light on a notions introduced later, on tacticals. The program in 
+Fig.\ref{fig:fun-pack-diff} %on p.\pageref{fig:fun-pack-diff}
+simplifies rational terms (typed as ``real'' due to limited development 
+resources):
+\begin{figure} [htb]
+  \centering
+  \includegraphics[width=0.95\textwidth]{fun-pack-simplify.png}
+ %\includegraphics[width=0.85\textwidth]{fig/scrshot/fun-pack/fun-pack-diff.png}
+  \caption{Simplification implemented by the function package}
+  \label{fig:fun-pack-diff}
+\end{figure}
+
+The program executes the tactic @{const Rewrite'_Set}\footnote{Isabelle's 
+document preparation system preserves the apostroph from the definition, while 
+Isabelle's pretty printer drops it in the presentation of the program as 
+above.}
+with different canonical term rewriting systems (called ``rule sets'' in 
+\sisac) guided by tacticals. The output (disregarding user interaction) is a 
+calculation with steps of simplification, where the steps are created by  
+@{const Rewrite'_Set}.
+
+Chained functions (by \texttt{\small \#>}) %TODO which antiquot?
+are applied curried to @{ML_type term}. The initial part of the chain, from 
+\texttt{\small ''discard\_minus''} to \texttt{\small ''cancel''} does 
+preprocessing, for instance replaces $\;a - b\;$ by $\;a + (-b)\;$ in 
+\texttt{\small ''discard\_minus''} for reducing 
+the number of theorems to be used in simplification.
+%
+The second chain of @{const Rewrite'_Set} is @{const Repeat}ed until no 
+further rewrites are possible; this is necessary in case of nested fractions.
+
+In cases like the one above, a confluent and terminating term rewrite system, 
+not only \emph{all} correct input terms are accepted, but also \emph{all} 
+incorrect input is rejected as @{term Not_Derivable} by the function  @{term 
+locate_input_term}.
+
+
+\section{Adaptation of Isabelle's Functions}\label{lucin-funpack}
+%=============================================================================
+Isabelle's function package presents functions in ``inner syntax'' to users, 
+i.e. as terms in Isabelle/HOL. The \LI{} design recognised these terms 
+suitable for parse trees of programs, Isabelle realised the same idea in a 
+more general way with the function package a few years later --- so migration 
+from \sisac's programs to Isabelle's functions was surprisingly easy. The main 
+features required were tactics, tacticals and program expressions as described 
+below.
+
+\subsection{Tactics Creating Steps in Calculations}\label{tactics}
+%-----------------------------------------------------------------------------
+The examples in the previous section showed how tactics in programs create 
+steps in calculations. Tactics in programs are defined as follows\footnote{
+\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/Prog_Tac.thy\#l36}}
+:
+\<close>
+consts
+  Calculate          :: "[char list, 'a] => 'a"
+  Rewrite            :: "[char list, 'a] => 'a"
+  Rewrite'_Inst      :: "[(char list * 'a) list, char list, 'a] => 'a"   
+  Rewrite'_Set       :: "[char list, 'a] => 'a"
+  Rewrite'_Set'_Inst :: "[((char list) * 'a) list, char list, 'a] => 'a"
+  Or'_to'_List       :: "bool => 'a list"
+  SubProblem         ::
+    "[char list * char list list * char list list, arg list] => 'a"
+  Substitute         :: "[bool list, 'a] => 'a"
+  Take               :: "'a => 'a"
+
+text \<open>
+These tactics transform a term of some type @{typ "'a"} to a resulting term of 
+the same type.  @{const[names_short] Calculate} applies operators like $+,-,*$ 
+as @{typ "char list"} (i.e. a string in inner syntax) to numerals of type  
+@{typ "'a"}. The tactics beginning with @{const[names_short] Rewrite} do 
+exactly what they indicate by applying a theorem (in the program given by type 
+@{typ "char list"}) or a list of theorems, called  ``rule-set''. The 
+corresponding \texttt{\small \_Inst} variants instantiate bound variables with 
+respective constants before rewriting (this is due to the user requirement, 
+that terms in calculations are close to traditional notation, which excludes 
+$\lambda$-terms), for instance modelling bound variables in equation solving. 
+@{const[names_short] Or'_to'_List} is due to a similar requirement: logically 
+appropriate for describing solution sets in equation solving are equalities 
+connected by $\land,\lor$, but traditional notation uses sets (and these are 
+still lists for convenience). @{const[names_short] SubProblem}s not only take 
+arguments (@{typ "arg list"} like any (sub-)program, but also three references 
+into \sisac's knowledge base  (theory, formal specification, method) for 
+guided interaction in the specification phase.
+
+Tactics appear simple: they operate on terms adhering to one type --- 
+different types are handled by different tactics and (sub-) programs; and they 
+cover only basic functionality --- but they operate on terms, which are well 
+tooled by Isabelle and which can contain functions evaluated as program 
+expressions introduced in the next but one subsection.
+
+Section \S\ref{expl-lucin} showed how tactics can be input by students. So 
+tactics in programs have analogies for user input with type @{ML_type 
+Tactic.input} defined at\footnote{
+\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/MathEngBasic/tactic-def.sml\#l122}}. These tactics also cover the specification phase (wich is out of scope of the 
+paper). And there is another @{ML_type Tactic.T} defined at\footnote{
+\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/MathEngBasic/tactic-def.sml\#l241}} for internal use by the mathematics-engine, which already appeared in the 
+signature of Lucas-Interpretation on p.\pageref{sig-lucin}.
+
+\subsection{Tacticals Guiding Flow of Execution}\label{tacticals}
+%-----------------------------------------------------------------------------
+The example on p.\pageref{expl-rewrite} for canonical rewriting showed, how 
+tacticals guide the flow of execution. The complete list of tacticals is as 
+follows.
+\<close>
+consts
+  Chain    :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10)
+  If       :: "[bool, 'a => 'a, 'a => 'a, 'a] => 'a"
+  Or       :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
+  Repeat   :: "['a => 'a, 'a] => 'a" 
+  Try      :: "['a => 'a, 'a] => 'a"
+  While    :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
+
+text \<open>
+\texttt{\small Chain}  is forward application of functions and made an infix 
+operator @{const[names_short] Chain}; @{const[names_short] If} decides by 
+@{typ bool}en expression for execution of one of two arguments of type @{typ 
+"'a => 'a"} (which can be combinations of tacticals or tactics); 
+@{const[names_short] Or} decides on execution of one of the arguments 
+depending of applicability of tactics; @{const[names_short] Repeat} is a one 
+way loop which terminates, if the argument is not applicable (e.g. 
+applicability of a theorem for rewriting on a term) any more; 
+@{const[names_short] Try} skips the argument if not applicable and 
+@{const[names_short] While} is a zero way loop as usual.
+
+\subsection{Program Expressions to be Evaluated}\label{prog-expr}
+%-----------------------------------------------------------------------------
+Some tacticals, \texttt{If} and \texttt{While}, involve boolean expressions, 
+which need to be evaluated: such expressions denote another element of 
+programs. This kind of element has been shown in the example on 
+p.\pageref{fig:fun-pack-biegelinie} as argument of  @{const[names_short] 
+Take}: sometimes it is necessary to pick parts of elements of a calculation, 
+for instance the last element from a list. So Isabelle's @{theory_text List} 
+is adapted for \sisac's purposes in @{theory_text ListC}\footnote{
+\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/ListC.thy}}.
+%
+Such expressions are substituted from the environment in @{ML_type Istate.T}, 
+evaluated to terms by rewriting (and for that purpose using the same rewrite 
+engine as for the tactics @{const[names_short] Rewrite}*) and marked by the 
+constructor @{term Term_Val} which is introduced below.
+
+
+\section{Implementation of \LI}\label{LI-impl}
+%=============================================================================
+The implementation of the interpreter is as experimental as is the respective 
+programming language introduced in the previous section. So below there will 
+be particularly such implementation details, which are required for discussing 
+open design \& implementation issues.
+
+All of the function package's syntactic part plus semantic markup is perfect 
+for \LI. The evaluation part of the function package, however, implements 
+automated evaluation in one go and automated 
+code-generation~\cite{code-gen-tutorial} --- both goals are not compatible 
+with \sisac's goal to feature step-wise construction of calculations, so this 
+part had to be done from scratch.
+
+
+\subsection{Scanning the Parse Tree}\label{scanning}
+%-----------------------------------------------------------------------------
+Isabelle's function package parses the program body from function definitions 
+to terms, the data structure of simply typed $\lambda$ terms, which also 
+encode the objects of proofs. Thus there is a remarkable collection of tools, 
+readily available in Isabelle; but this collection does not accommodate the 
+requirement of scanning a term to a certain location, remembering the location 
+and returning there later, as required by \LI. So this has been introduced
+\<close> 
+(*<*)ML(*>*) \<open>
+datatype lrd = L | R | D
+type path = lrd list
+\<close> 
+(*<*)ML \<open>
+open TermC (*avoids type clashes below from the new typ above*)
+\<close> 
+    ML(*>*) \<open>
+fun at_location [] t = t
+  | at_location (D :: p) (Abs(_, _, body)) = at_location p body
+  | at_location (L :: p) (t1 $ _) = at_location p t1
+  | at_location (R :: p) (_ $ t2) = at_location p t2
+  | at_location l t =
+    raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]);
+\<close>
+text \<open>
+with a @{term path} to a location according to the term constructors 
+\texttt{\small \$} and @{term Abs}. This is an implementation detail; an 
+abstract, denotational view starts with this datatype
+\<close> 
+(*<*)ML(*>*) \<open>
+datatype expr_val =
+    Term_Val of term  | Reject_Tac
+  | Accept_Tac of Istate.pstate * Proof.context * Tactic.T
+\<close>
+text \<open>
+which models the meaning of an expression in the parse-tree: this is either a  
+@{term Term_Val}ue  (introduced in \S\ref{prog-expr}) or a tactic (introduced 
+in \S\ref{tactics}); the latter is either accepted by  @{term Accept_Tac} or 
+rejected by  @{term Reject_Tac}; an error value is still missing.
+%
+The arguments of the above constant @{term Accept_Tac} are the same as 
+introduced for \LI{} in \S\ref{concept-LI}. Thus @{ML_type expr_val} is the 
+return value for functions scanning the parse-tree for an acceptable tactic:
+\<close> 
+(*<*)ML \<open>
+open LI (*avoids type clashes below from the new typ above*)
+\<close> 
+    ML(*>*) \<open>
+scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val;
+scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val;
+go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val;
+scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val;
+check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> 
+expr_val;
+\<close>
+text \<open>
+The first argument of each function above, if of type  @{ML_type term}, is the 
+whole program. It is not required by @{term scan_dn}, simple top-down 
+scanning, and by @{term check_tac}, if a tactic has been reached. The 
+rightmost argument, if of type  @{ML_type term}, serves matching as shown 
+later. @{term scan_to_tactic} recognises, whether interpretation is just 
+starting a new program (@{term "path = []"}) or interpretation resumes at a 
+certain location:
+\<close> 
+(*<*)ML \<open>
+open Celem
+open LI
+\<close> 
+    ML(*>*) \<open>
+fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) =
+    if path = []
+    then scan_dn cc (ist |> set_path [R]) (Program.body_of prog)
+    else go_scan_up (prog, cc) ist
+  | scan_to_tactic _ _ =
+    raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
+\<close>
+    text \<open>
+@{term scan_dn} sets the path in the interpreter state @{term ist} to @{term 
+R}, the program body, while @{term go_scan_up} goes one level up the path in 
+order to call @{term go_scan_up}. Both functions, scanning down and up, are 
+shown below\footnote{
+Referring to the example in Fig.\ref{fig:fun-pack-diff} on 
+p.\pageref{fig:fun-pack-diff} we show the interpreter code only for tacticals 
+@{const[names_short] Try}, @{const[names_short] Repeat} and chaining 
+\texttt{\small \#>} (which is \texttt{\small "Tactical.Chain"} in the code). 
+We also omit the cases for uncurried application, which only occurs once (in 
+the first, i.e. the out-most @{const[names_short] Try}) in the example.
+}:
+\<close> 
+(*<*)ML(*>*) \<open>
+fun scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try", _) $ e) =
+    (case scan_dn cc (ist |> path_down [R]) e of
+      Reject_Tac => Term_Val act_arg
+    | goback => goback)
+  | scan_dn cc ist (Const ("Tactical.Repeat", _) $ e) =
+    scan_dn cc (ist |> path_down [R]) e
+  | scan_dn cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
+    (case scan_dn cc (ist |> path_down [L, R]) e1 of
+	    Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2
+    | goback => goback)
+(*|*)
+  | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t =
+    if Tactical.contained_in t
+    then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])
+    else
+      case LItool.check_leaf "next  " ctxt eval (get_subst ist) t of
+  	    (Program.Expr s, _) => Term_Val s
+      | (Program.Tac prog_tac, form_arg) =>
+          check_tac cc ist (prog_tac, form_arg)
+\<close>
+    text \<open>
+The last case of @{term scan_dn} must have reached a leaf. @{term check_leaf} 
+distinguishes between @{term Expr} and @{term Tac}; the former returns a 
+@{term Term_Val}, the latter returns the result of @{term check_tac} called by 
+@{term scan_dn}, where the result is either @{term Accept_Tac} or @{term 
+Reject_Tac}. In case of  @{term Accept_Tac} scanning is stalled (in 
+\S\ref{expl-lucin} such a tactic has been called a beak-point), the respective 
+tactic is returned (together with corresponding @{ML_type Istate.T} and 
+@{ML_type Proof.context}) to the mathematics-engine. 
+In case of @{term Reject_Tac} an explicit back tracking by @{term scan_up} 
+tries other branches with @{term scan_dn}.
+
+\medskip
+@{term scan_up} is as simple as @{term scan_dn}; an essential difference is, 
+that the former requires the whole program for @{term go_scan_up} as follows:
+\<close> 
+(*<*)ML(*>*) \<open>
+fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept,...})=
+    if path = [R]
+    then
+      if found_accept then Term_Val act_arg else Reject_Tac
+    else 
+      scan_up pcc (ist |> path_up) (go_up path sc)
+and scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist
+  | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
+    (case scan_dn cc (ist |> path_down [R]) e of
+      Accept_Tac ict => Accept_Tac ict
+    | Reject_Tac => go_scan_up pcc ist
+    | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
+  | scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) =
+    go_scan_up pcc ist
+  | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =
+      let 
+        val e2 = check_Seq_up ist sc
+      in
+        case scan_dn cc (ist |> path_up_down [R]) e2 of
+          Accept_Tac ict => Accept_Tac ict
+        | Reject_Tac => go_scan_up pcc (ist |> path_up)
+        | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> 
+set_found)
+      end
+(*|*)
+\<close>
+text \<open>
+\subsection{Use of Isabelle's Contexts}\label{ctxt}
+%-----------------------------------------------------------------------------
+Isabelle's \textit{``logical context represents the background that is 
+required for formulating statements and composing proofs. It acts as a medium 
+to produce formal content, depending on earlier material (declarations, 
+results etc.).''} \cite{implem-tutorial}. The \sisac-prototype introduced 
+Isabelle's @{ML_structure Context} in collaboration with a 
+student~\cite{mlehnf:bakk-11}, now uses them throughout construction of 
+problem solutions and implements a specific structure @{ML_structure 
+ContextC}\footnote{A closing ``C'' indicates an \sisac{} extension, see 
+{\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/00612574cbfd/src/Tools/isac/CalcElements/contextC.sml}}}.
+
+At the beginning of the specification phase (briefly touched by tactic 
+@{term[names_short] SubProblem} in \S\ref{expl-lucin} and explained in little 
+more detail in the subsequent section) an Isabelle theory must be specified, 
+this is followed by \texttt{\small Proof\_Context.init\_global} in the 
+specification module. Then \texttt{\small Proof\_Context.initialise'} takes a 
+formalisation of the problem as strings, which are parsed by \texttt{\small  
+Syntax.read\_term} using the context, and finally the resulting term's types 
+are recorded in the context by \texttt{\small Variable.declare\_constraints}. 
+The latter relieves students from type constraints for input terms. Finally, 
+as soon as a problem type is specified, the respective preconditions are 
+stored by \texttt{\small ContextC.insert\_assumptions}.
+
+\medskip
+During \LI{} the context is updated with assumptions generated by conditional 
+rewriting and by switching to and from sub-programs. An example for the former 
+is tactic  @{term[names_short] SubProblem} applied with theorem $x \ne 0 
+\Rightarrow (\frac{a}{x} = b) = (a = b\cdot x)$ during equation solving.
+
+A still not completely solved issue is switching to and from 
+@{term[names_short] SubProblem}s; the scope of an interpreter's environment is 
+different from a logical context's scope. When calling a sub-program, \sisac{} 
+uses \texttt{\small Proof\_Context.initialise}, but returning execution from a 
+@{term[names_short] SubProblem} is not so clear. For instance, if such a 
+sub-program determined the solutions $[x=0,\;x=\sqrt{2}]$, while the calling 
+program maintains the assumption $x\not=0$ from above, then the solution $x=0$ 
+must be dropped, this is clear. But how determine in full generality, which 
+context data to consider when returning execution to a calling program? 
+Presently the decision in \texttt{\small 
+ContextC.subpbl\_to\_caller}\footnote{
+\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/ce071aa3eae4/src/Tools/isac/CalcElements/contextC.sml\#l73}} 
+is, to transfer all content data which contain at least one variable of the 
+calling program and drop them on contradiction.
+
+\subsection{Guarding and Embedding Execution}\label{embedding}
+%-----------------------------------------------------------------------------
+Guardin
+
+@{theory_text partial_function}s as used by \LI{} are alien to HOL for 
+fundamental reasons. And when the \sisac-project started with the aim to 
+support learning mathematics as taught at engineering faculties, it was clear, 
+that formal specifications should guard execution of programs under \LI{} 
+(i.e. execution only starts, when the specification's preconditions evaluate 
+to true).
+
+So formal specification is required for technical reasons \emph{and} for 
+educational reasons in engineering education. The \sisac-project designed a 
+separate specification phase, where input to a problem and corresponding 
+output as well as preconditions and post-condition are handled explicitly by 
+students; example in  Fig.\ref{fig:fun-pack-biegelinie} shows several 
+@{term[names_short] SubProblem}s, which lead to mutual recursion between 
+specification phase and phases creating a solution (supported by \LI).
+
+\paragraph{Embedding} \LI{} into a dialogue-module is required in order to 
+meet user requirements in educational settings. Looking at the calculation 
+shown on p.\pageref{biegel_calc} and considering the power of the three 
+mainfunction (1)\dots(3) mentioned in the respective comment on 
+p.\pageref{1-2-3}, it is clear, that in particular @{term[names_short] 
+find_next_step} needs control: The dialogue-module hands over control to a 
+student at each step of \LI, but students should also be warned against using 
+a button creating the next step too frequently. A careful reduction of help 
+from \LI{} might make the learning system also usable for written exams.
+
+\<close>
+
+(*<*)
+end
+(*>*)              
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/Lucas_Interpreter/document/bend-7-70-en.png
Binary file src/Tools/isac/Doc/Lucas_Interpreter/document/bend-7-70-en.png has changed
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/Lucas_Interpreter/document/fun-pack-biegelinie-2.png
Binary file src/Tools/isac/Doc/Lucas_Interpreter/document/fun-pack-biegelinie-2.png has changed
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/Lucas_Interpreter/document/fun-pack-simplify.png
Binary file src/Tools/isac/Doc/Lucas_Interpreter/document/fun-pack-simplify.png has changed
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/Lucas_Interpreter/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.bib	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,351 @@
+
+@Proceedings{EPTCS79,
+  title = 	 {{\rm Proceedings First Workshop on}
+               CTP Components for Educational Software (THedu'11)},
+  year = 	 {2012},
+  booktitle = {Electronic Proceedings in Theoretical Computer Science},
+  editor    = "Quaresma, Pedro and Back, Ralph-Johan",
+  volume    = "79",
+  publisher = "Open Publishing Association"
+}
+@techreport{RISC5885,
+author = {David M. Cerna},
+title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
+year = {2019},
+month = {Feburary},
+length = {17},
+type = {RISC Report Series},
+institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
+address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
+}
+@Article{EMS-STT-19,
+  author = {Koichu, Boris and Pinto, Alon},
+  title = {The Seoncdary-Tertiary Transition in Mathematics. What are our current challenges and what can we do about them?},
+  journal = {EMS Newsletter},
+  year = {2019},
+  pages = {34-35},
+  month = {June},
+  doi = {10.4171/NEWS}
+}
+
+@Inproceedings{EPTCS290.6,
+  author    = {Neuper, Walther},
+  year      = {2019},
+  title     = {Technologies for "Complete, Transparent \& Interactive Models of Math" in Education},
+  editor    = {Quaresma, Pedro and Neuper, Walther},
+  booktitle = {{\rm Proceedings 7th International Workshop on}
+               Theorem proving components for Educational software,
+               {\rm Oxford, United Kingdom, 18 july 2018}},
+  series    = {Electronic Proceedings in Theoretical Computer Science},
+  volume    = {290},
+  publisher = {Open Publishing Association},
+  pages     = {76-95},
+  doi       = {10.4204/EPTCS.290.6}
+}
+@InProceedings{wneuper:gcd-coimbra,
+  author = 	 {Neuper, Walther},
+  title = 	 {{GCD} --- A Case Study on {L}ucas-Interpretation},
+  booktitle = {Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM},
+  year = 	 {2014},
+  address = 	 {Coimbra, Portugal},
+  month = 	 {July 7-11},
+  note = 	 {\url{http://ceur-ws.org/Vol-1186/paper-17.pdf}}
+}
+@Article{flip-class-meta,
+  author = {Shi, Y. and Ma, Y. and MacLeod, J. and others},
+  title = {College students’ cognitive learning outcomes in flipped classroom instruction: a meta-analysis of the empirical literature},
+  journal = {Journal of Computers in Education},
+  year = {2019},
+  pages = {1-25},
+  month = {May},
+  doi = {https://doi.org/10.1007/s40692-019-00142-8}
+}
+@inproceedings{krauss,
+  author    = {Krauss, Alexander},
+  title     = {Partial Recursive Functions in Higher-Order Logic},
+  pages     = {589-603},
+  doi       = {10.1007/11814771\_48},
+  editor    = {Ulrich Furbach and Natarajan Shankar},
+  booktitle     = {Automated Reasoning, Third International Joint Conference, IJCAR 2006},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {4130},
+  year      = {2006},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@Manual{funpack-tutorial,
+  title = 	 {Defining Recursive Functions in {Isabelle/HOL}},
+  author = 	 {Alexander Krauss},
+  address = 	 {Munich},
+  year = 	 {},
+  note = 	 {{P}art of the Isabelle distribution},
+  url = 	 {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
+}
+@Misc{nipkow-prog-prove-ny,
+  author = 	 {Nipkow, Tobias},
+  title = 	 {Programming and Proving in {Isabelle/HOL}},
+  howpublished = {contained in the Isabelle distribution},
+  year = 	 {},
+  url = 	 {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}
+}
+@Misc{code-gen-tutorial,
+  author = 	 {Florian Haftmann},
+  title = 	 {Code generation from {Isabelle/HOL} theories},
+  howpublished = {Contained in the Isabelle distribution},
+  year = 	 {},
+  url = 	 {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}
+}
+@Misc{implem-tutorial,
+  author = 	 {Makarius Wenzel},
+  title = 	 {The {Isabelle/Isar} Implementation},
+  howpublished = {Contained in the Isabelle distribution},
+  year = 	 {},
+  url = 	 {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}
+}
+@Misc{sledgehammer-tutorial,
+  author = 	 {Jasmin C.Blanchette},
+  title = 	 {{Hammering Away. A User's Guide to Sledgehammer for Isabelle/HOL}},
+  howpublished = {contained in the Isabelle distribution},
+  year = 	 {},
+  url = 	 {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
+}
+@incollection {haftm-nipkow-code-gen-HRS-10,
+   author = {Haftmann, Florian and Nipkow, Tobias},
+   affiliation = {Institut für Informatik, Technische Universität München},
+   title = {Code Generation via Higher-Order Rewrite Systems},
+   booktitle = {Functional and Logic Programming},
+   series = {Lecture Notes in Computer Science},
+   editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germán},
+   publisher = {Springer Berlin / Heidelberg},
+   isbn = {978-3-642-12250-7},
+   keyword = {Computer Science},
+   pages = {103-117},
+   volume = {6009},
+   url = {http://dx.doi.org/10.1007/978-3-642-12251-4\_9},
+   doi = {10.1007/978-3-642-12251-4\_9},
+   year = {2010}
+}
+@misc{url-afp,
+  title = {Archive of {F}ormal {P}roofs},
+  howpublished = {\url{http://afp.sourceforge.net}}
+}
+@incollection {Cogent-to-C-2016,
+   author = {S. Amani and A. Hixon and Z. Chen and C. Rizkallah and P. Chubb and L. O’Connor and
+J. Beeren and Y. Nagashima and J. Lim and T. Sewell and J. Tuong and G. Keller and T. Murray and 
+G. Klein and G. Heiser},
+   title = {Cogent: Verifying High-Assurance File System Implementations},
+   booktitle = {International Conference on Architectural Support for Programming Languages and
+Operating Systems},
+   publisher = {Springer Berlin / Heidelberg},
+   address = {Atlanta, GA, USA},
+   pages = {175-188},
+   doi = {10.1145/2872362.2872404},
+   year = {2016}
+}
+@InProceedings{wn:proto-sys,
+  author    = {Krempler, Alan and Neuper, Walther},
+  year      = {2018},
+  title     = {Prototyping ``Systems that Explain Themselves'' for Education},
+  editor    = {Quaresma, Pedro and Neuper, Walther},
+  booktitle = {{\rm Proceedings 6th International Workshop on}
+               Theorem proving components for Educational software,
+               {\rm Gothenburg, Sweden, 6 Aug 2017}},
+  series    = {Electronic Proceedings in Theoretical Computer Science},
+  volume    = {267},
+  publisher = {Open Publishing Association},
+  pages     = {89-107},
+  doi       = {10.4204/EPTCS.267.6}
+}
+@Book{Isa-tutor08,
+  author = 	 {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},
+  title = 	 {Isabelle/HOL, a proof assistant for high-order logic},
+  publisher = 	 {Springer Verlag},
+  year = 	 {2008}
+}
+@InCollection{pl:formal-lang-hist,
+  author = 	 {Lucas, Peter},
+  title = 	 {On the Formalization of Programming Languages: Early History and Main Approaches},
+  booktitle = 	 {The Vienna Development Method: The Meta-Language},
+  publisher = {Springer},
+  year = 	 {1978},
+  editor = 	 {D. Bj{\o}rner and C. B. Jones},
+  volume = 	 {16},
+  series = 	 {LNCS},
+  doi = {10.1007/3-540-08766-4\_8}
+}
+@InProceedings{thedu16:lucin-user-view,
+  author = 	 {Neuper, Walther},
+  title = 	 {Lucas-Interpretation from Users' Perspective},
+  booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program,
+and Work in Progress at the Conference on Intelligent Computer Mathematics},
+  year = 	 {2016},
+  address = {Bialystok, Poland},
+  month = {July 25-29},
+  pages = {83-89},
+  note = {\url{http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf}}
+}
+@Misc{wn:lucin-thedu18,
+  author = 	 {Walther Neuper},
+  title = 	 {Lucas-Interpretation from Programmers' Perspective},
+  year = 	 {2018},
+  note = {Abstract for ThEdu'18 \url{http://www.ist.tugraz.at/projects/isac/publ/lucin-prog-view.pdf}}
+}
+@InProceedings{wn:lucas-interp-12,
+  author    = "Neuper, Walther",
+  year      = "2012",
+  title     = "Automated Generation of User Guidance by Combining Computation and Deduction",
+  pages     = "82-101",
+  doi       = "10.4204/EPTCS.79.5",
+  booktitle = {Electronic Proceedings in Theoretical Computer Science},
+  editor    = "Quaresma, Pedro and Back, Ralph-Johan",
+  volume    = "79",
+  publisher = "Open Publishing Association"
+}
+@Book{progr-mathematica-2012,
+  author = 	 {Maeder, Roman E.},
+  title = 	 {Programming in Mathematica},
+  publisher = 	 {Addison-Wesley},
+  address = 	 {Reading, Mass.},
+  year = 	 {2012},
+  edition = 	 {3rd}
+}
+@PhdThesis{wn:diss,
+  author = 	 {Neuper, Walther },
+  title = 	 {Reactive User-Guidance by an Autonomous Engine Doing High-School Math},
+  school = 	 {IICM - Inst. f. Softwaretechnology},
+  year = 	 {2001},
+  address = 	 {Technical University, A-8010 Graz},
+  note = 	{\url{http://www.ist.tugraz.at/projects/isac/publ/wn-diss.ps.gz}}
+}
+@Article{plmms10,
+  author = 	 {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
+  title = 	 {{CTP}-based programming languages~? {C}onsiderations about an experimental design},
+  journal = 	 {ACM Communications in Computer Algebra},
+  doi = {10.1145/1838599.1838621},
+  year = 	 {2010},
+  volume = 	 {44},
+  number = 	 {1/2},
+  pages = 	 {27-41},
+  month = 	 {March/June}
+}
+@Article{back-SD-2010,
+  author = 	 {R.-J. Back},
+  title = 	 {Structured derivations: a unified proof style for teaching mathematics},
+  journal = 	 {Formal Aspects of Computing},
+  year = 	 {2010},
+  volume = 	 {22},
+  number = 	 {5},
+  pages = 	 {629-661}
+}
+@MastersThesis{mlehnf:bakk-11,
+  author = 	 {Mathias Lehnfeld},
+  title = 	 {Verbindung von 'Computation' und 'Deduction' im \sisac-System},
+  school = 	 {Institut f\"ur Computersprachen, Technische Universit\"at Wien},
+  year = 	 {2011},
+  note = 	 {Bakkalaureate project}
+}
+@incollection{paulson700,
+  author        = {Lawrence C. Paulson},
+  title         = {{Isabelle}: The Next 700 Theorem Provers},
+  booktitle     = {Logic and Computer Science},
+  editor        = {P. Odifreddi},
+  pages         = {361-386},
+  publisher     = {Academic Press},
+  url           = {https://arxiv.org/abs/cs/9301106},
+  year          = {1990}
+}
+@misc{RISC4777,
+    author = {B. Buchberger},
+    title = {{The Role of Mathematical Thinking for 21st Century Society}},
+    language = {english},
+    year = {2013},
+    month = {March 4-6},
+    annote = {2013-03-04-A},
+    note = {Invited talk at The 2nd International Conference on Mathematics and Technology in Mathematics Education},
+    institution = {Khemarak University, Phnom Penh, Cambodia},
+    conferencename = {The 2nd International Conference on Mathematics and Technology in Mathematics Education}
+}
+@Article{EMS-math-ethics,
+  author = {Chiodo, Maurice and Clifton, Toby},
+  title = {The Importance of Ethics in Mathematics},
+  journal = {Newsletter of the European Mathematical Society},
+  year = {2019},
+  volume = {114},
+  pages = {34-37},
+  month = {December},
+  url = {\url{https://euro-math-soc.eu/newsletter}}
+}
+@MastersThesis{ggt02,
+  author = 	 {Karnel, Stefan},
+  title = 	 {Gr\"o{\ss}te gemeinsame Teiler in Polynomringen und Implementierung im \isac-Projekt},
+  school = 	 {University of Technology, Institute of Mathematics},
+  year = 	 {2002},
+  address = 	 {Graz, Austria},
+  month = 	 {Aug}
+}
+@InProceedings{gdaroczy-EP-13,
+  author = 	 {Gabriella Dar\'{o}czy and Walther Neuper},
+  title = 	 {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},
+  booktitle = 	 {eJMT, the Electronic Journal of Mathematics \& Technology},
+  year = 	 {2013},
+  volume = 	 {7},
+  pages = 	 {175-194},
+  month = 	 {February},
+  note = 	 {Special Issue ``TP-based Systems and Education''},
+  url = {\url{https://php.radford.edu/~ejmt/ContentIndex.php\#v7n2}}
+}
+@TECHREPORT{tBaBoEr07a,
+  author = {Back, Ralph-Johan and Bos, Victor and Eriksson, Johannes},
+  title = {MathEdit: Tool Support for Structured Calculational Proofs},
+  institution = {TUCS},
+  year = {2007},
+  number = {854},
+  month = {Dec},
+  note = {\url{http://tucs.fi/publications/view/?pub_id=tBaBoEr07a}}
+}
+@article{Farmer_al:93,
+author = {W. D. Farmer and J. D. Guttman and F. J. Thayer},
+title = {{IMPS: An Interactive Mathematical Proof System}},
+journal = {Journal of Automated Reasoning},
+year = {1993},
+volume = {11},
+month = {August},
+number = {2},
+pages = {213-248},
+}
+@InProceedings{gclc-06,
+  author = 	 {Jani\v{c}i\'c, Predrag},
+  title = 	 {{GCLC} --- a tool for constructive euclidean geometry and more than that},
+  booktitle =    {Mathematical Software -- {ICMS} 2006},
+  pages = 	 {58-73},
+  year = 	 {2006},
+  number = 	 {4151}
+}
+@Article{ggb:atp-15,
+  author = 	 {Botana, F. and Hohenwarter, M. and Jani\v{c}i\'c, P. and Kov\'acs, Z. and Petrovi\'c, I. and Recio, T. and Weitzhofer, S.},
+  title = 	 {Automated Theorem Proving in {GeoGebra}: Current Achievements},
+  journal = 	 {Journal of Automated Reasoning},
+  year = 	 {2015},
+  volume = 	 {55},
+  number = 	 {1},
+  pages = 	 {39-59},
+  ISSN = 	 {0168-7433},
+  DOI = 	 {http://dx.doi.org/10.1007/s10817-015-9326-4}
+}
+@Manual{isabelle-jedit,
+  title = 	 {{Isabelle/jEdit}},
+  author = 	 {Makarius Wenzel},
+  address = 	 {Munich},
+  note = 	 {Part of the Isabelle distribution},
+  note = 	 {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}
+}
+@TechReport{Yacc-1975,
+  author = {Johnson, Stephen C.},
+  title = {Yacc: {Y}et {A}nother {C}ompiler-{C}ompiler},
+  institution = {AT\&T Bell Laboratories},
+  year = {1975},
+  number = {32},
+  address = {Murray Hill, New Jersey},
+  note = {Retrieved 31 January 2020}
+}
+
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:
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/README	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,7 @@
+~~/src/Tools/isac/Doc/README
+
+pdflatex in ~~/src/Tools/isac/Doc/ by:
+/usr/local/isabisac/bin/isabelle build -D .
+ 
+In case nothing happens with the above command, go
+~/.isabelle/isabisac/heaps/polyml-5.8_x86_64_32-linux/log$ rm Lucas_Interpreter*
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/ROOT	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,16 @@
+session "Lucas_Interpreter" in "Lucas_Interpreter" = HOL +
+  options [document = pdf, document_output = "output"]
+  sessions
+    "Interpret"
+  theories
+    "Lucas_Interpreter"
+  document_files (in "../")
+    "isabelle.sty"
+    "isabellesym.sty"
+    "pdfsetup.sty"
+  document_files
+    "bend-7-70-en.png"
+    "fun-pack-biegelinie-2.png"
+    "fun-pack-simplify.png"
+    "root.bib"
+    "root.tex"
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/comment.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/comment.sty	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,278 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Comment.sty   version 3.6, October 1999
+%
+% Purpose:
+% selectively in/exclude pieces of text: the user can define new
+% comment versions, and each is controlled separately.
+% Special comments can be defined where the user specifies the
+% action that is to be taken with each comment line.
+%
+% Author
+%    Victor Eijkhout
+%    Department of Computer Science
+%    University of Tennessee
+%    107 Ayres Hall
+%    Knoxville TN 37996
+%    USA
+%
+%    victor@eijkhout.net
+%
+% This program is free software; you can redistribute it and/or
+% modify it under the terms of the GNU General Public License
+% as published by the Free Software Foundation; either version 2
+% of the License, or (at your option) any later version.
+% 
+% This program is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+% GNU General Public License for more details.
+%
+% For a copy of the GNU General Public License, write to the 
+% Free Software Foundation, Inc.,
+% 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA,
+% or find it on the net, for instance at
+% http://www.gnu.org/copyleft/gpl.html
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% This style can be used with plain TeX or LaTeX, and probably
+% most other packages too.
+%
+% Usage: all text included between
+%    \comment ... \endcomment
+% or \begin{comment} ... \end{comment}
+% is discarded. 
+%
+% The opening and closing commands should appear on a line
+% of their own. No starting spaces, nothing after it.
+% This environment should work with arbitrary amounts
+% of comment, and the comment can be arbitrary text.
+%
+% Other `comment' environments are defined by
+% and are selected/deselected with
+% \includecomment{versiona}
+% \excludecoment{versionb}
+%
+% These environments are used as
+% \versiona ... \endversiona
+% or \begin{versiona} ... \end{versiona}
+% with the opening and closing commands again on a line of 
+% their own.
+%
+% LaTeX users note: for an included comment, the
+% \begin and \end lines act as if they don't exist.
+% In particular, they don't imply grouping, so assignments 
+% &c are not local.
+%
+% Special comments are defined as
+% \specialcomment{name}{before commands}{after commands}
+% where the second and third arguments are executed before
+% and after each comment block. You can use this for global
+% formatting commands.
+% To keep definitions &c local, you can include \begingroup
+% in the `before commands' and \endgroup in the `after commands'.
+% ex:
+% \specialcomment{smalltt}
+%     {\begingroup\ttfamily\footnotesize}{\endgroup}
+% You do *not* have to do an additional
+% \includecomment{smalltt}
+% To remove 'smalltt' blocks, give \excludecomment{smalltt}
+% after the definition.
+%
+% Processing comments can apply processing to each line.
+% \processcomment{name}{each-line commands}%
+%    {before commands}{after commands}
+% By defining a control sequence 
+% \def\Thiscomment##1{...} in the before commands the user can
+% specify what is to be done with each comment line.
+% BUG this does not work quite yet BUG
+%
+% Trick for short in/exclude macros (such as \maybe{this snippet}):
+%\includecomment{cond}
+%\newcommand{\maybe}[1]{}
+%\begin{cond}
+%\renewcommand{\maybe}[1]{#1}
+%\end{cond}
+%
+% Basic approach of the implementation:
+% to comment something out, scoop up  every line in verbatim mode
+% as macro argument, then throw it away.
+% For inclusions, in LaTeX the block is written out to
+% a file \CommentCutFile (default "comment.cut"), which is
+% then included.
+% In plain TeX (and other formats) both the opening and
+% closing comands are defined as noop.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Changes in version 3.1
+% - updated author's address
+% - cleaned up some code
+% - trailing contents on \begin{env} line is always discarded
+%  even if you've done \includecomment{env}
+% - comments no longer define grouping!! you can even
+%   \includecomment{env}
+%   \begin{env}
+%   \begin{itemize}
+%   \end{env}
+%  Isn't that something ...
+% - included comments are written to file and input again.
+% Changes in 3.2
+% - \specialcomment brought up to date (thanks to Ivo Welch).
+% Changes in 3.3
+% - updated author's address again
+% - parametrised \CommentCutFile
+% Changes in 3.4
+% - added GNU public license
+% - added \processcomment, because Ivo's fix (above) brought an
+%   inconsistency to light.
+% Changes in 3.5
+% - corrected typo in header.
+% - changed author email
+% - corrected \specialcomment yet again.
+% - fixed excludecomment of an earlier defined environment.
+% Changes in 3.6
+% - The 'cut' file is now written more verbatim, using \meaning;
+%   some people reported having trouble with ISO latin 1, or umlaute.sty.
+% - removed some \newif statements.
+%   Has this suddenly become \outer again?
+%
+% Known bugs:
+% - excludecomment leads to one superfluous space
+% - processcomment leads to a superfluous line break
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\makeinnocent#1{\catcode`#1=12 }
+\def\csarg#1#2{\expandafter#1\csname#2\endcsname}
+\def\latexname{lplain}\def\latexename{LaTeX2e}
+\newwrite\CommentStream
+\def\CommentCutFile{comment.cut}
+
+\def\ProcessComment#1% start it all of
+   {\begingroup
+    \def\CurrentComment{#1}%
+    \let\do\makeinnocent \dospecials 
+    \makeinnocent\^^L% and whatever other special cases
+    \endlinechar`\^^M \catcode`\^^M=12 \xComment}
+%\def\ProcessCommentWithArg#1#2% to be used in \leveledcomment
+%   {\begingroup
+%    \def\CurrentComment{#1}%
+%    \let\do\makeinnocent \dospecials 
+%    \makeinnocent\^^L% and whatever other special cases
+%    \endlinechar`\^^M \catcode`\^^M=12 \xComment}
+{\catcode`\^^M=12 \endlinechar=-1 %
+ \gdef\xComment#1^^M{%
+    \expandafter\ProcessCommentLine}
+ \gdef\ProcessCommentLine#1^^M{\def\test{#1}
+      \csarg\ifx{End\CurrentComment Test}\test
+          \edef\next{\noexpand\EndOfComment{\CurrentComment}}%
+      \else \ThisComment{#1}\let\next\ProcessCommentLine
+      \fi \next}
+}
+
+\def\CSstringmeaning#1{\expandafter\CSgobblearrow\meaning#1}
+\def\CSstringcsnoescape#1{\expandafter\CSgobbleescape\string#1}
+{\escapechar-1
+\expandafter\expandafter\expandafter\gdef
+  \expandafter\expandafter\expandafter\CSgobblearrow
+    \expandafter\string\csname macro:->\endcsname{}
+}
+\def\CSgobbleescape#1{\ifnum`\\=`#1 \else #1\fi}
+\def\WriteCommentLine#1{\def\CStmp{#1}%
+    \immediate\write\CommentStream{\CSstringmeaning\CStmp}}
+
+% 3.1 change: in LaTeX and LaTeX2e prevent grouping
+\if 0%
+\ifx\fmtname\latexename 
+    0%
+\else \ifx\fmtname\latexname 
+          0%
+      \else 
+          1%
+\fi   \fi
+%%%%
+%%%% definitions for LaTeX
+%%%%
+\def\AfterIncludedComment
+   {\immediate\closeout\CommentStream
+    \input{\CommentCutFile}\relax
+    }%
+\def\TossComment{\immediate\closeout\CommentStream}
+\def\BeforeIncludedComment
+   {\immediate\openout\CommentStream=\CommentCutFile
+    \let\ThisComment\WriteCommentLine}
+\def\includecomment
+ #1{\message{Include comment '#1'}%
+    \csarg\let{After#1Comment}\AfterIncludedComment
+    \csarg\def{#1}{\BeforeIncludedComment
+        \ProcessComment{#1}}%
+    \CommentEndDef{#1}}
+\long\def\specialcomment
+ #1#2#3{\message{Special comment '#1'}%
+    % note: \AfterIncludedComment does \input, so #2 goes here!
+    \csarg\def{After#1Comment}{#2\AfterIncludedComment#3}%
+    \csarg\def{#1}{\BeforeIncludedComment\relax
+          \ProcessComment{#1}}%
+    \CommentEndDef{#1}}
+\long\def\processcomment
+ #1#2#3#4{\message{Lines-Processing comment '#1'}%
+    \csarg\def{After#1Comment}{#3\AfterIncludedComment#4}%
+    \csarg\def{#1}{\BeforeIncludedComment#2\relax
+          \ProcessComment{#1}}%
+    \CommentEndDef{#1}}
+\def\leveledcomment
+ #1#2{\message{Include comment '#1' up to level '#2'}%
+    %\csname #1IsLeveledCommenttrue\endcsname
+    \csarg\let{After#1Comment}\AfterIncludedComment
+    \csarg\def{#1}{\BeforeIncludedComment
+        \ProcessCommentWithArg{#1}}%
+    \CommentEndDef{#1}}
+\else 
+%%%%
+%%%%plain TeX and other formats
+%%%%
+\def\includecomment
+ #1{\message{Including comment '#1'}%
+    \csarg\def{#1}{}%
+    \csarg\def{end#1}{}}
+\long\def\specialcomment
+ #1#2#3{\message{Special comment '#1'}%
+    \csarg\def{#1}{\def\ThisComment{}\def\AfterComment{#3}#2%
+           \ProcessComment{#1}}%
+    \CommentEndDef{#1}}
+\fi
+
+%%%%
+%%%% general definition of skipped comment
+%%%%
+\def\excludecomment
+ #1{\message{Excluding comment '#1'}%
+    \csarg\def{#1}{\let\AfterComment\relax
+           \def\ThisComment####1{}\ProcessComment{#1}}%
+    \csarg\let{After#1Comment}\TossComment
+    \CommentEndDef{#1}}
+
+\if 0%
+\ifx\fmtname\latexename 
+    0%
+\else \ifx\fmtname\latexname 
+          0%
+      \else 
+          1%
+\fi   \fi
+% latex & latex2e:
+\def\EndOfComment#1{\endgroup\end{#1}%
+    \csname After#1Comment\endcsname}
+\def\CommentEndDef#1{{\escapechar=-1\relax
+    \csarg\xdef{End#1Test}{\string\\end\string\{#1\string\}}%
+    }}
+\else
+% plain & other
+\def\EndOfComment#1{\endgroup\AfterComment}
+\def\CommentEndDef#1{{\escapechar=-1\relax
+    \csarg\xdef{End#1Test}{\string\\end#1}%
+    }}
+\fi
+
+\excludecomment{comment}
+
+\endinput
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/isabelle.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/isabelle.sty	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,269 @@
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language and symbols)
+
+% isabelle environments
+
+\newcommand{\isabellecontext}{UNKNOWN}
+\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
+
+\newcommand{\isastyle}{\UNDEF}
+\newcommand{\isastylett}{\UNDEF}
+\newcommand{\isastyleminor}{\UNDEF}
+\newcommand{\isastyleminortt}{\UNDEF}
+\newcommand{\isastylescript}{\UNDEF}
+\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
+\newcommand{\isastyletxt}{\normalfont\rmfamily}
+\newcommand{\isastylecmt}{\normalfont\rmfamily}
+
+\newcommand{\isaspacing}{%
+  \sfcode 42 1000 % .
+  \sfcode 63 1000 % ?
+  \sfcode 33 1000 % !
+  \sfcode 58 1000 % :
+  \sfcode 59 1000 % ;
+  \sfcode 44 1000 % ,
+}
+
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
+\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
+\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
+\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
+
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+
+\newenvironment{isabellebody}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isaspacing\isastyle}{\par}
+
+\newenvironment{isabellebodytt}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isaspacing\isastylett}{\par}
+
+\newenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\item\relax}
+{\end{isabellebody}\end{trivlist}}
+
+\newenvironment{isabellett}
+{\begin{trivlist}\begin{isabellebodytt}\item\relax}
+{\end{isabellebodytt}\end{trivlist}}
+
+\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
+\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
+
+\newcommand{\isaindent}[1]{\hphantom{#1}}
+\newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isasep}{}
+\newcommand{\isadigit}[1]{#1}
+
+\newcommand{\isachardefaults}{%
+\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
+\chardef\isacharbang=`\!%
+\chardef\isachardoublequote=`\"%
+\chardef\isachardoublequoteopen=`\"%
+\chardef\isachardoublequoteclose=`\"%
+\chardef\isacharhash=`\#%
+\chardef\isachardollar=`\$%
+\chardef\isacharpercent=`\%%
+\chardef\isacharampersand=`\&%
+\chardef\isacharprime=`\'%
+\chardef\isacharparenleft=`\(%
+\chardef\isacharparenright=`\)%
+\chardef\isacharasterisk=`\*%
+\chardef\isacharplus=`\+%
+\chardef\isacharcomma=`\,%
+\chardef\isacharminus=`\-%
+\chardef\isachardot=`\.%
+\chardef\isacharslash=`\/%
+\chardef\isacharcolon=`\:%
+\chardef\isacharsemicolon=`\;%
+\chardef\isacharless=`\<%
+\chardef\isacharequal=`\=%
+\chardef\isachargreater=`\>%
+\chardef\isacharquery=`\?%
+\chardef\isacharat=`\@%
+\chardef\isacharbrackleft=`\[%
+\chardef\isacharbackslash=`\\%
+\chardef\isacharbrackright=`\]%
+\chardef\isacharcircum=`\^%
+\chardef\isacharunderscore=`\_%
+\def\isacharunderscorekeyword{\_}%
+\chardef\isacharbackquote=`\`%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
+\chardef\isacharbraceleft=`\{%
+\chardef\isacharbar=`\|%
+\chardef\isacharbraceright=`\}%
+\chardef\isachartilde=`\~%
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
+\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
+\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+}
+
+
+% keyword and section markup
+
+\newcommand{\isakeyword}[1]
+{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
+
+\newcommand{\isakeywordcontrol}[1]
+{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
+
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
+\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
+
+\newif\ifisamarkup
+\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
+\newcommand{\isaendpar}{\par\medskip}
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
+\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% styles
+
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestyledefault}{%
+\def\isastyle{\small\normalfont\ttfamily\slshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
+\def\isastyleminortt{\small\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
+\isachardefaults%
+}
+\isabellestyledefault
+
+\newcommand{\isabellestylett}{%
+\def\isastyle{\small\normalfont\ttfamily}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\small\normalfont\ttfamily}%
+\def\isastyleminortt{\small\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\ttfamily}%
+\isachardefaults%
+}
+
+\newcommand{\isabellestyleit}{%
+\def\isastyle{\small\normalfont\itshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\normalfont\itshape}%
+\def\isastyleminortt{\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\itshape}%
+\isachardefaults%
+\def\isacharunderscorekeyword{\mbox{-}}%
+\def\isacharbang{\isamath{!}}%
+\def\isachardoublequote{}%
+\def\isachardoublequoteopen{}%
+\def\isachardoublequoteclose{}%
+\def\isacharhash{\isamath{\#}}%
+\def\isachardollar{\isamath{\$}}%
+\def\isacharpercent{\isamath{\%}}%
+\def\isacharampersand{\isamath{\&}}%
+\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\def\isacharparenleft{\isamath{(}}%
+\def\isacharparenright{\isamath{)}}%
+\def\isacharasterisk{\isamath{*}}%
+\def\isacharplus{\isamath{+}}%
+\def\isacharcomma{\isamath{\mathord,}}%
+\def\isacharminus{\isamath{-}}%
+\def\isachardot{\isamath{\mathord.}}%
+\def\isacharslash{\isamath{/}}%
+\def\isacharcolon{\isamath{\mathord:}}%
+\def\isacharsemicolon{\isamath{\mathord;}}%
+\def\isacharless{\isamath{<}}%
+\def\isacharequal{\isamath{=}}%
+\def\isachargreater{\isamath{>}}%
+\def\isacharat{\isamath{@}}%
+\def\isacharbrackleft{\isamath{[}}%
+\def\isacharbackslash{\isamath{\backslash}}%
+\def\isacharbrackright{\isamath{]}}%
+\def\isacharunderscore{\mbox{-}}%
+\def\isacharbraceleft{\isamath{\{}}%
+\def\isacharbar{\isamath{\mid}}%
+\def\isacharbraceright{\isamath{\}}}%
+\def\isachartilde{\isamath{{}\sp{\sim}}}%
+\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
+\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\def\isacharverbatimopen{\isamath{\langle\!\langle}}%
+\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
+}
+
+\newcommand{\isabellestyleliteral}{%
+\isabellestyleit%
+\def\isacharunderscore{\_}%
+\def\isacharunderscorekeyword{\_}%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
+}
+
+\newcommand{\isabellestyleliteralunderscore}{%
+\isabellestyleliteral%
+\def\isacharunderscore{\textunderscore}%
+\def\isacharunderscorekeyword{\textunderscore}%
+}
+
+\newcommand{\isabellestylesl}{%
+\isabellestyleit%
+\def\isastyle{\small\normalfont\slshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\normalfont\slshape}%
+\def\isastyleminortt{\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\slshape}%
+}
+
+
+% cancel text
+
+\usepackage[normalem]{ulem}
+\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
+
+
+% tagged regions
+
+%plain TeX version of comment package -- much faster!
+\let\isafmtname\fmtname\def\fmtname{plain}
+\usepackage{comment}
+\let\fmtname\isafmtname
+
+\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
+
+\newcommand{\isakeeptag}[1]%
+{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isadroptag}[1]%
+{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isafoldtag}[1]%
+{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
+
+\isakeeptag{document}
+\isakeeptag{theory}
+\isakeeptag{proof}
+\isakeeptag{ML}
+\isakeeptag{visible}
+\isadroptag{invisible}
+\isakeeptag{important}
+\isakeeptag{unimportant}
+
+\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/isabellesym.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/isabellesym.sty	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,417 @@
+%%
+%% definitions of standard Isabelle symbols
+%%
+
+\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb
+\newcommand{\isasymone}{\isamath{\mathbf{1}}}  %requires amssymb
+\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}  %requires amssymb
+\newcommand{\isasymthree}{\isamath{\mathbf{3}}}  %requires amssymb
+\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb
+\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb
+\newcommand{\isasymsix}{\isamath{\mathbf{6}}}  %requires amssymb
+\newcommand{\isasymseven}{\isamath{\mathbf{7}}}  %requires amssymb
+\newcommand{\isasymeight}{\isamath{\mathbf{8}}}  %requires amssymb
+\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb
+\newcommand{\isasymA}{\isamath{\mathcal{A}}}
+\newcommand{\isasymB}{\isamath{\mathcal{B}}}
+\newcommand{\isasymC}{\isamath{\mathcal{C}}}
+\newcommand{\isasymD}{\isamath{\mathcal{D}}}
+\newcommand{\isasymE}{\isamath{\mathcal{E}}}
+\newcommand{\isasymF}{\isamath{\mathcal{F}}}
+\newcommand{\isasymG}{\isamath{\mathcal{G}}}
+\newcommand{\isasymH}{\isamath{\mathcal{H}}}
+\newcommand{\isasymI}{\isamath{\mathcal{I}}}
+\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
+\newcommand{\isasymK}{\isamath{\mathcal{K}}}
+\newcommand{\isasymL}{\isamath{\mathcal{L}}}
+\newcommand{\isasymM}{\isamath{\mathcal{M}}}
+\newcommand{\isasymN}{\isamath{\mathcal{N}}}
+\newcommand{\isasymO}{\isamath{\mathcal{O}}}
+\newcommand{\isasymP}{\isamath{\mathcal{P}}}
+\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
+\newcommand{\isasymR}{\isamath{\mathcal{R}}}
+\newcommand{\isasymS}{\isamath{\mathcal{S}}}
+\newcommand{\isasymT}{\isamath{\mathcal{T}}}
+\newcommand{\isasymU}{\isamath{\mathcal{U}}}
+\newcommand{\isasymV}{\isamath{\mathcal{V}}}
+\newcommand{\isasymW}{\isamath{\mathcal{W}}}
+\newcommand{\isasymX}{\isamath{\mathcal{X}}}
+\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
+\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
+\newcommand{\isasyma}{\isamath{\mathrm{a}}}
+\newcommand{\isasymb}{\isamath{\mathrm{b}}}
+\newcommand{\isasymc}{\isamath{\mathrm{c}}}
+\newcommand{\isasymd}{\isamath{\mathrm{d}}}
+\newcommand{\isasyme}{\isamath{\mathrm{e}}}
+\newcommand{\isasymf}{\isamath{\mathrm{f}}}
+\newcommand{\isasymg}{\isamath{\mathrm{g}}}
+\newcommand{\isasymh}{\isamath{\mathrm{h}}}
+\newcommand{\isasymi}{\isamath{\mathrm{i}}}
+\newcommand{\isasymj}{\isamath{\mathrm{j}}}
+\newcommand{\isasymk}{\isamath{\mathrm{k}}}
+\newcommand{\isasyml}{\isamath{\mathrm{l}}}
+\newcommand{\isasymm}{\isamath{\mathrm{m}}}
+\newcommand{\isasymn}{\isamath{\mathrm{n}}}
+\newcommand{\isasymo}{\isamath{\mathrm{o}}}
+\newcommand{\isasymp}{\isamath{\mathrm{p}}}
+\newcommand{\isasymq}{\isamath{\mathrm{q}}}
+\newcommand{\isasymr}{\isamath{\mathrm{r}}}
+\newcommand{\isasyms}{\isamath{\mathrm{s}}}
+\newcommand{\isasymt}{\isamath{\mathrm{t}}}
+\newcommand{\isasymu}{\isamath{\mathrm{u}}}
+\newcommand{\isasymv}{\isamath{\mathrm{v}}}
+\newcommand{\isasymw}{\isamath{\mathrm{w}}}
+\newcommand{\isasymx}{\isamath{\mathrm{x}}}
+\newcommand{\isasymy}{\isamath{\mathrm{y}}}
+\newcommand{\isasymz}{\isamath{\mathrm{z}}}
+\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
+\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
+\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
+\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
+\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
+\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
+\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
+\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
+\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
+\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
+\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
+\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
+\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
+\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
+\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
+\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
+\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
+\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
+\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
+\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
+\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
+\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
+\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
+\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
+\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
+\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
+\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
+\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
+\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
+\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
+\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
+\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
+\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
+\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
+\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
+\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
+\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
+\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
+\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
+\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
+\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
+\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
+\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
+\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
+\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
+\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
+\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
+\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
+\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
+\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
+\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
+\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
+\newcommand{\isasymalpha}{\isamath{\alpha}}
+\newcommand{\isasymbeta}{\isamath{\beta}}
+\newcommand{\isasymgamma}{\isamath{\gamma}}
+\newcommand{\isasymdelta}{\isamath{\delta}}
+\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
+\newcommand{\isasymzeta}{\isamath{\zeta}}
+\newcommand{\isasymeta}{\isamath{\eta}}
+\newcommand{\isasymtheta}{\isamath{\vartheta}}
+\newcommand{\isasymiota}{\isamath{\iota}}
+\newcommand{\isasymkappa}{\isamath{\kappa}}
+\newcommand{\isasymlambda}{\isamath{\lambda}}
+\newcommand{\isasymmu}{\isamath{\mu}}
+\newcommand{\isasymnu}{\isamath{\nu}}
+\newcommand{\isasymxi}{\isamath{\xi}}
+\newcommand{\isasympi}{\isamath{\pi}}
+\newcommand{\isasymrho}{\isamath{\varrho}}
+\newcommand{\isasymsigma}{\isamath{\sigma}}
+\newcommand{\isasymtau}{\isamath{\tau}}
+\newcommand{\isasymupsilon}{\isamath{\upsilon}}
+\newcommand{\isasymphi}{\isamath{\varphi}}
+\newcommand{\isasymchi}{\isamath{\chi}}
+\newcommand{\isasympsi}{\isamath{\psi}}
+\newcommand{\isasymomega}{\isamath{\omega}}
+\newcommand{\isasymGamma}{\isamath{\Gamma}}
+\newcommand{\isasymDelta}{\isamath{\Delta}}
+\newcommand{\isasymTheta}{\isamath{\Theta}}
+\newcommand{\isasymLambda}{\isamath{\Lambda}}
+\newcommand{\isasymXi}{\isamath{\Xi}}
+\newcommand{\isasymPi}{\isamath{\Pi}}
+\newcommand{\isasymSigma}{\isamath{\Sigma}}
+\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
+\newcommand{\isasymPhi}{\isamath{\Phi}}
+\newcommand{\isasymPsi}{\isamath{\Psi}}
+\newcommand{\isasymOmega}{\isamath{\Omega}}
+\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
+\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
+\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
+\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
+\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
+\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
+\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
+\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
+\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
+\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}}  %requires amsmath
+\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}}  %requires amsmath
+\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}}  %requires amsmath
+\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}}  %requires amsmath
+\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
+\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
+\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}}  %requires amssymb
+\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}}  %requires amssymb
+\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
+\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
+\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
+\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
+\newcommand{\isasymmapsto}{\isamath{\mapsto}}
+\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
+\newcommand{\isasymmidarrow}{\isamath{\relbar}}
+\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
+\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
+\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
+\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
+\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
+\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
+\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
+\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
+\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb
+\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb
+\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb
+\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb
+\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
+\newcommand{\isasymup}{\isamath{\uparrow}}
+\newcommand{\isasymUp}{\isamath{\Uparrow}}
+\newcommand{\isasymdown}{\isamath{\downarrow}}
+\newcommand{\isasymDown}{\isamath{\Downarrow}}
+\newcommand{\isasymupdown}{\isamath{\updownarrow}}
+\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
+\newcommand{\isasymlangle}{\isamath{\langle}}
+\newcommand{\isasymrangle}{\isamath{\rangle}}
+\newcommand{\isasymlceil}{\isamath{\lceil}}
+\newcommand{\isasymrceil}{\isamath{\rceil}}
+\newcommand{\isasymlfloor}{\isamath{\lfloor}}
+\newcommand{\isasymrfloor}{\isamath{\rfloor}}
+\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
+\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
+\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
+\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
+\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
+\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
+\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
+\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
+\newcommand{\isasymbottom}{\isamath{\bot}}
+\newcommand{\isasymtop}{\isamath{\top}}
+\newcommand{\isasymand}{\isamath{\wedge}}
+\newcommand{\isasymAnd}{\isamath{\bigwedge}}
+\newcommand{\isasymor}{\isamath{\vee}}
+\newcommand{\isasymOr}{\isamath{\bigvee}}
+\newcommand{\isasymforall}{\isamath{\forall\,}}
+\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymnot}{\isamath{\neg}}
+\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
+\newcommand{\isasymcircle}{\isamath{\ocircle}}  %requires wasysym
+\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
+\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
+\newcommand{\isasymdiamondop}{\isamath{\diamond}}
+\newcommand{\isasymsurd}{\isamath{\surd}}
+\newcommand{\isasymturnstile}{\isamath{\vdash}}
+\newcommand{\isasymTurnstile}{\isamath{\models}}
+\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
+\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
+\newcommand{\isasymstileturn}{\isamath{\dashv}}
+\newcommand{\isasymle}{\isamath{\le}}
+\newcommand{\isasymge}{\isamath{\ge}}
+\newcommand{\isasymlless}{\isamath{\ll}}
+\newcommand{\isasymggreater}{\isamath{\gg}}
+\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
+\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
+\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
+\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
+\newcommand{\isasymin}{\isamath{\in}}
+\newcommand{\isasymnotin}{\isamath{\notin}}
+\newcommand{\isasymsubset}{\isamath{\subset}}
+\newcommand{\isasymsupset}{\isamath{\supset}}
+\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
+\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb
+\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
+\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
+\newcommand{\isasyminter}{\isamath{\cap}}
+\newcommand{\isasymInter}{\isamath{\bigcap\,}}
+\newcommand{\isasymunion}{\isamath{\cup}}
+\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
+\newcommand{\isasymsqunion}{\isamath{\sqcup}}
+\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
+\newcommand{\isasymsqinter}{\isamath{\sqcap}}
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymuplus}{\isamath{\uplus}}
+\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
+\newcommand{\isasymnoteq}{\isamath{\not=}}
+\newcommand{\isasymsim}{\isamath{\sim}}
+\newcommand{\isasymdoteq}{\isamath{\doteq}}
+\newcommand{\isasymsimeq}{\isamath{\simeq}}
+\newcommand{\isasymapprox}{\isamath{\approx}}
+\newcommand{\isasymasymp}{\isamath{\asymp}}
+\newcommand{\isasymcong}{\isamath{\cong}}
+\newcommand{\isasymsmile}{\isamath{\smile}}
+\newcommand{\isasymequiv}{\isamath{\equiv}}
+\newcommand{\isasymfrown}{\isamath{\frown}}
+\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb
+\newcommand{\isasymbowtie}{\isamath{\bowtie}}
+\newcommand{\isasymprec}{\isamath{\prec}}
+\newcommand{\isasymsucc}{\isamath{\succ}}
+\newcommand{\isasympreceq}{\isamath{\preceq}}
+\newcommand{\isasymsucceq}{\isamath{\succeq}}
+\newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymplusminus}{\isamath{\pm}}
+\newcommand{\isasymminusplus}{\isamath{\mp}}
+\newcommand{\isasymtimes}{\isamath{\times}}
+\newcommand{\isasymdiv}{\isamath{\div}}
+\newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymstar}{\isamath{\star}}
+\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
+\newcommand{\isasymcirc}{\isamath{\circ}}
+\newcommand{\isasymdagger}{\isamath{\dagger}}
+\newcommand{\isasymddagger}{\isamath{\ddagger}}
+\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb
+\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb
+\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb
+\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb
+\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
+\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
+\newcommand{\isasymtriangle}{\isamath{\triangle}}
+\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
+\newcommand{\isasymoplus}{\isamath{\oplus}}
+\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
+\newcommand{\isasymotimes}{\isamath{\otimes}}
+\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
+\newcommand{\isasymodot}{\isamath{\odot}}
+\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
+\newcommand{\isasymominus}{\isamath{\ominus}}
+\newcommand{\isasymoslash}{\isamath{\oslash}}
+\newcommand{\isasymdots}{\isamath{\dots}}
+\newcommand{\isasymcdots}{\isamath{\cdots}}
+\newcommand{\isasymSum}{\isamath{\sum\,}}
+\newcommand{\isasymProd}{\isamath{\prod\,}}
+\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
+\newcommand{\isasyminfinity}{\isamath{\infty}}
+\newcommand{\isasymintegral}{\isamath{\int\,}}
+\newcommand{\isasymointegral}{\isamath{\oint\,}}
+\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
+\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
+\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
+\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
+\newcommand{\isasymaleph}{\isamath{\aleph}}
+\newcommand{\isasymemptyset}{\isamath{\emptyset}}
+\newcommand{\isasymnabla}{\isamath{\nabla}}
+\newcommand{\isasympartial}{\isamath{\partial}}
+\newcommand{\isasymRe}{\isamath{\Re}}
+\newcommand{\isasymIm}{\isamath{\Im}}
+\newcommand{\isasymflat}{\isamath{\flat}}
+\newcommand{\isasymnatural}{\isamath{\natural}}
+\newcommand{\isasymsharp}{\isamath{\sharp}}
+\newcommand{\isasymangle}{\isamath{\angle}}
+\newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}}
+\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
+\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}}  %requires textcomp
+\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}}  %requires textcomp
+\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}}  %requires textcomp
+\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}}
+\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}}
+\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}}
+\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}}
+\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}}
+\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}}
+\newcommand{\isasymeuro}{\isatext{\euro}}  %requires eurosym
+\newcommand{\isasympounds}{\isamath{\pounds}}
+\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
+\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
+\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
+\newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}}  %requires textcomp
+\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}}
+\newcommand{\isasymamalg}{\isamath{\amalg}}
+\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
+\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
+\newcommand{\isasymwp}{\isamath{\wp}}
+\newcommand{\isasymwrong}{\isamath{\wr}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
+\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
+\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
+\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
+\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
+\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
+\newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
+\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
+
+\newcommand{\isactrlmarker}{\isatext{\ding{48}}}  %requires pifont
+\newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
+\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
+\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
+\newcommand{\isactrlclass}{\isakeywordcontrol{class}}
+\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}
+\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}}
+\newcommand{\isactrlconst}{\isakeywordcontrol{const}}
+\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}}
+\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}}
+\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}}
+\newcommand{\isactrlcontext}{\isakeywordcontrol{context}}
+\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}}
+\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}}
+\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}}
+\newcommand{\isactrldir}{\isakeywordcontrol{dir}}
+\newcommand{\isactrlfile}{\isakeywordcontrol{file}}
+\newcommand{\isactrlhere}{\isakeywordcontrol{here}}
+\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
+\newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
+\newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
+\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
+\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
+\newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
+\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}
+\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}
+\newcommand{\isactrlpath}{\isakeywordcontrol{path}}
+\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}}
+\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
+\newcommand{\isactrlprint}{\isakeywordcontrol{print}}
+\newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
+\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
+\newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
+\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
+\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}}
+\newcommand{\isactrlterm}{\isakeywordcontrol{term}}
+\newcommand{\isactrltheory}{\isakeywordcontrol{theory}}
+\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}}
+\newcommand{\isactrltyp}{\isakeywordcontrol{typ}}
+\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}}
+\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}}
+\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}}
+\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}}
+
+\newcommand{\isactrlcode}{\isakeywordcontrol{code}}
+\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}
+\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}
+\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/isabelletags.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/isabelletags.sty	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,1 @@
+
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/pdfsetup.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/pdfsetup.sty	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,7 @@
+%%
+%% default hyperref setup (both for pdf and dvi output)
+%%
+
+\usepackage{color}
+\definecolor{linkcolor}{rgb}{0,0,0.5}
+\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,urlcolor=linkcolor,pdfpagelabels]{hyperref}
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/Doc/railsetup.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/railsetup.sty	Wed Mar 11 15:25:52 2020 +0100
@@ -0,0 +1,1202 @@
+% rail.sty - style file to support railroad diagrams
+%
+% 09-Jul-90 L. Rooijakkers
+% 08-Oct-90 L. Rooijakkers	fixed centering bug when \rail@tmpc<0.
+% 07-Feb-91 L. Rooijakkers	added \railoptions command, indexing
+% 08-Feb-91 L. Rooijakkers	minor fixes
+% 28-Jun-94 K. Barthelmann	turned into LaTeX2e package
+% 08-Dec-96 K. Barthelmann	replaced \@writefile
+% 13-Dec-96 K. Barthelmann	cleanup
+% 22-Feb-98 K. Barthelmann	fixed catcodes of special characters
+% 18-Apr-98 K. Barthelmann	fixed \par handling
+% 19-May-98 J. Olsson		Added new macros to support arrow heads.
+% 26-Jul-98 K. Barthelmann	changed \par to output newlines
+% 02-May-11 M. Wenzel           default setup for Isabelle
+%
+% This style file needs to be used in conjunction with the 'rail'
+% program. Running LaTeX as 'latex file' produces file.rai, which should be
+% processed by Rail with 'rail file'. This produces file.rao, which will
+% be picked up by LaTeX on the next 'latex file' run.
+%
+% LaTeX will warn if there is no file.rao or it's out of date.
+%
+% The macros in this file thus consist of two parts: those that read and
+% write the .rai and .rao files, and those that do the actual formatting
+% of the railroad diagrams.
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{rail}[1998/05/19]
+
+% railroad diagram formatting parameters (user level)
+% all of these are copied into their internal versions by \railinit
+%
+% \railunit : \unitlength within railroad diagrams
+% \railextra : extra length at outside of diagram
+% \railboxheight : height of ovals and frames
+% \railboxskip : vertical space between lines
+% \railboxleft : space to the left of a box
+% \railboxright : space to the right of a box
+% \railovalspace : extra space around contents of oval
+% \railframespace : extra space around contents of frame
+% \railtextleft : space to the left of text
+% \railtextright : space to the right of text
+% \railtextup : space to lift text up
+% \railjoinsize : circle size of join/split arcs
+% \railjoinadjust : space to adjust join
+%
+% \railnamesep : separator between name and rule body
+
+\newlength\railunit
+\newlength\railextra
+\newlength\railboxheight
+\newlength\railboxskip
+\newlength\railboxleft
+\newlength\railboxright
+\newlength\railovalspace
+\newlength\railframespace
+\newlength\railtextleft
+\newlength\railtextright
+\newlength\railtextup
+\newlength\railjoinsize
+\newlength\railjoinadjust
+\newlength\railnamesep
+
+% initialize the parameters
+
+\setlength\railunit{1sp}
+\setlength\railextra{4ex}
+\setlength\railboxleft{1ex}
+\setlength\railboxright{1ex}
+\setlength\railovalspace{2ex}
+\setlength\railframespace{2ex}
+\setlength\railtextleft{1ex}
+\setlength\railtextright{1ex}
+\setlength\railjoinadjust{0pt}
+\setlength\railnamesep{1ex}
+
+\DeclareOption{10pt}{
+  \setlength\railboxheight{16pt}
+  \setlength\railboxskip{24pt}
+  \setlength\railtextup{5pt}
+  \setlength\railjoinsize{16pt}
+}
+\DeclareOption{11pt}{
+  \setlength\railboxheight{16pt}
+  \setlength\railboxskip{24pt}
+  \setlength\railtextup{5pt}
+  \setlength\railjoinsize{16pt}
+}
+\DeclareOption{12pt}{
+  \setlength\railboxheight{20pt}
+  \setlength\railboxskip{28pt}
+  \setlength\railtextup{6pt}
+  \setlength\railjoinsize{20pt}
+}
+
+\ExecuteOptions{10pt}
+\ProcessOptions
+
+% internal versions of the formatting parameters
+%
+% \rail@extra   : \railextra
+% \rail@boxht   : \railboxheight
+% \rail@boxsp   : \railboxskip
+% \rail@boxlf   : \railboxleft
+% \rail@boxrt   : \railboxright
+% \rail@boxhht  : \railboxheight / 2
+% \rail@ovalsp  : \railovalspace
+% \rail@framesp : \railframespace
+% \rail@textlf  : \railtextleft
+% \rail@textrt  : \railtextright
+% \rail@textup  : \railtextup
+% \rail@joinsz  : \railjoinsize
+% \rail@joinhsz : \railjoinsize / 2
+% \rail@joinadj : \railjoinadjust
+%
+% \railinit : internalize all of the parameters.
+
+\newcount\rail@extra
+\newcount\rail@boxht
+\newcount\rail@boxsp
+\newcount\rail@boxlf
+\newcount\rail@boxrt
+\newcount\rail@boxhht
+\newcount\rail@ovalsp
+\newcount\rail@framesp
+\newcount\rail@textlf
+\newcount\rail@textrt
+\newcount\rail@textup
+\newcount\rail@joinsz
+\newcount\rail@joinhsz
+\newcount\rail@joinadj
+
+\newcommand\railinit{
+\rail@extra=\railextra
+\divide\rail@extra by \railunit
+\rail@boxht=\railboxheight
+\divide\rail@boxht by \railunit
+\rail@boxsp=\railboxskip
+\divide\rail@boxsp by \railunit
+\rail@boxlf=\railboxleft
+\divide\rail@boxlf by \railunit
+\rail@boxrt=\railboxright
+\divide\rail@boxrt by \railunit
+\rail@boxhht=\railboxheight
+\divide\rail@boxhht by \railunit
+\divide\rail@boxhht by 2
+\rail@ovalsp=\railovalspace
+\divide\rail@ovalsp by \railunit
+\rail@framesp=\railframespace
+\divide\rail@framesp by \railunit
+\rail@textlf=\railtextleft
+\divide\rail@textlf by \railunit
+\rail@textrt=\railtextright
+\divide\rail@textrt by \railunit
+\rail@textup=\railtextup
+\divide\rail@textup by \railunit
+\rail@joinsz=\railjoinsize
+\divide\rail@joinsz by \railunit
+\rail@joinhsz=\railjoinsize
+\divide\rail@joinhsz by \railunit
+\divide\rail@joinhsz by 2
+\rail@joinadj=\railjoinadjust
+\divide\rail@joinadj by \railunit
+}
+
+\AtBeginDocument{\railinit}
+
+% \rail@param : declarations for list environment
+%
+% \railparam{TEXT} : sets \rail@param to TEXT
+%
+% \rail@reserved : characters reserved for grammar
+
+\newcommand\railparam[1]{
+\def\rail@param{
+  \setlength\leftmargin{0pt}\setlength\rightmargin{0pt}
+  \setlength\labelwidth{0pt}\setlength\labelsep{0pt}
+  \setlength\itemindent{0pt}\setlength\listparindent{0pt}
+  #1
+}
+}
+\railparam{}
+
+\newtoks\rail@reserved
+\rail@reserved={:;|*+?[]()'"}
+
+% \rail@termfont : format setup for terminals
+%
+% \rail@nontfont : format setup for nonterminals
+%
+% \rail@annofont : format setup for annotations
+%
+% \rail@rulefont : format setup for rule names
+%
+% \rail@indexfont : format setup for index entry
+%
+% \railtermfont{TEXT} : set terminal format setup to TEXT
+%
+% \railnontermfont{TEXT} : set nonterminal format setup to TEXT
+%
+% \railannotatefont{TEXT} : set annotation format setup to TEXT
+%
+% \railnamefont{TEXT} : set rule name format setup to TEXT
+%
+% \railindexfont{TEXT} : set index entry format setup to TEXT
+
+\def\rail@termfont{\ttfamily\upshape}
+\def\rail@nontfont{\rmfamily\upshape}
+\def\rail@annofont{\rmfamily\itshape}
+\def\rail@namefont{\rmfamily\itshape}
+\def\rail@indexfont{\rmfamily\itshape}
+
+\newcommand\railtermfont[1]{
+\def\rail@termfont{#1}
+}
+
+\newcommand\railnontermfont[1]{
+\def\rail@nontfont{#1}
+}
+
+\newcommand\railannotatefont[1]{
+\def\rail@annofont{#1}
+}
+
+\newcommand\railnamefont[1]{
+\def\rail@namefont{#1}
+}
+
+\newcommand\railindexfont[1]{
+\def\rail@indexfont{#1}
+}
+
+% railroad read/write macros
+%
+% \begin{rail} TEXT \end{rail} : TEXT is written out to the .rai file,
+%                                as \rail@i{NR}{TEXT}. Then the matching
+%                                \rail@o{NR}{FMT} from the .rao file is
+%                                executed (if defined).
+%
+% \railoptions{OPTIONS} : OPTIONS are written out to the .rai file,
+%                         as \rail@p{OPTIONS}.
+%
+% \railterm{IDENT,IDENT,...} : format IDENT as terminals. writes out
+%                              \rail@t{IDENT} to the .rai file
+%
+% \railalias{IDENT}{TEXT} : format IDENT as TEXT. defines \rail@t@IDENT as
+%                           TEXT.
+%
+% \railtoken{IDENT}{TEXT} : abbreviates \railalias{IDENT}{TEXT}\railterm{IDENT}
+%                           (for backward compatibility)
+%
+% \rail@setcodes : guards special characters
+%
+% \rail@makeother{CHARACTER} : sets \catcode of CHARACTER to "other"
+%                              used inside a loop for \rail@setcodes
+%
+% \rail@nr : railroad diagram counter
+%
+% \ifrail@match : current \rail@i{NR}{TEXT} matches
+%
+% \rail@first : actions to be done first. read in .rao file,
+%               open .rai file if \@filesw true, undefine \rail@first.
+%               executed from \begin{rail}, \railoptions and \railterm.
+%
+% \rail@i{NR}{TEXT} : defines \rail@i@NR as TEXT. written to the .rai
+%                     file by \rail, read from the .rao file by
+%                     \rail@first
+%
+% \rail@t{IDENT} : tells Rail that IDENT is to be custom formatted,
+%                  written to the .rai file by \railterm.
+%
+% \rail@o{NR}{TEXT} : defines \rail@o@NR as TEXT, read from the .rao
+%                     file by \rail@first.
+%
+% \rail@p{OPTIONS} : pass options to rail, written to the .rai file by
+%                    \railoptions
+%
+% \rail@write{TEXT} : write TEXT to the .rai file
+%
+% \rail@warn : warn user for mismatching diagrams
+%
+% \rail@endwarn : either \relax or \rail@warn
+%
+% \ifrail@all : checked at the end of the document
+
+\def\rail@makeother#1{
+  \expandafter\catcode\expandafter`\csname\string #1\endcsname=12
+}
+
+\def\rail@setcodes{
+\let\par=\relax
+\let\\=\relax
+\expandafter\@tfor\expandafter\rail@symbol\expandafter:\expandafter=%
+  \the\rail@reserved
+\do{\expandafter\rail@makeother\rail@symbol}
+}
+
+\newcount\rail@nr
+
+\newif\ifrail@all
+\rail@alltrue
+
+\newif\ifrail@match
+
+\def\rail@first{
+\begingroup
+\makeatletter
+\rail@setcodes
+\InputIfFileExists{\jobname.rao}{}{\PackageInfo{rail}{No file \jobname.rao}}
+\makeatother
+\endgroup
+\if@filesw
+\newwrite\tf@rai
+\immediate\openout\tf@rai=\jobname.rai
+\fi
+\global\let\rail@first=\relax
+}
+
+\long\def\rail@body#1\end{
+{
+\newlinechar=`^^J
+\def\par{\string\par^^J}
+\rail@write{\string\rail@i{\number\rail@nr}{#1}}
+}
+\xdef\rail@i@{#1}
+\end
+}
+
+\newenvironment{rail}{
+\global\advance\rail@nr by 1
+\rail@first
+\begingroup
+\rail@setcodes
+\rail@body
+}{
+\endgroup
+\rail@matchtrue
+\@ifundefined{rail@o@\number\rail@nr}{\rail@matchfalse}{}
+\expandafter\ifx\csname rail@i@\number\rail@nr\endcsname\rail@i@
+\else
+\rail@matchfalse
+\fi
+\ifrail@match
+\csname rail@o@\number\rail@nr\endcsname
+\else
+\PackageWarning{rail}{Railroad diagram {\number\rail@nr} doesn't match}
+\global\let\rail@endwarn=\rail@warn
+\begin{list}{}{\rail@param}
+\rail@begin{1}{}
+\rail@setbox{\bfseries ???}
+\rail@oval
+\rail@end
+\end{list}
+\fi
+}
+
+\newcommand\railoptions[1]{
+\rail@first
+\rail@write{\string\rail@p{#1}}
+}
+
+\newcommand\railterm[1]{
+\rail@first
+\@for\rail@@:=#1\do{
+\rail@write{\string\rail@t{\rail@@}}
+}
+}
+
+\newcommand\railalias[2]{
+\expandafter\def\csname rail@t@#1\endcsname{#2}
+}
+
+\newcommand\railtoken[2]{\railalias{#1}{#2}\railterm{#1}}
+
+\long\def\rail@i#1#2{
+\expandafter\gdef\csname rail@i@#1\endcsname{#2}
+}
+
+\def\rail@o#1#2{
+\expandafter\gdef\csname rail@o@#1\endcsname{
+\begin{list}{}{\rail@param}
+#2
+\end{list}
+}
+}
+
+\def\rail@t#1{}
+
+\def\rail@p#1{}
+
+\long\def\rail@write#1{\@ifundefined{tf@rai}{}{\immediate\write\tf@rai{#1}}}
+
+\def\rail@warn{
+\PackageWarningNoLine{rail}{Railroad diagram(s) may have changed.
+                            Use 'rail' and rerun}
+}
+
+\let\rail@endwarn=\relax
+
+\AtEndDocument{\rail@endwarn}
+
+% index entry macro
+%
+% \rail@index{IDENT} : add index entry for IDENT
+
+\def\rail@index#1{
+\index{\rail@indexfont#1}
+}
+
+% railroad formatting primitives
+%
+% \rail@x : current x
+% \rail@y : current y
+% \rail@ex : current end x
+% \rail@sx : starting x for \rail@cr
+% \rail@rx : rightmost previous x for \rail@cr
+%
+% \rail@tmpa : temporary count
+% \rail@tmpb : temporary count
+% \rail@tmpc : temporary count
+%
+% \rail@put : put at (\rail@x,\rail@y)
+% \rail@vput : put vector at (\rail@x,\rail@y)
+%
+% \rail@eline : end line by drawing from \rail@ex to \rail@x
+%
+% \rail@vreline : end line by drawing a vector from \rail@x to \rail@ex
+%
+% \rail@vleline : end line by drawing a vector from \rail@ex to \rail@x
+%
+% \rail@sety{LEVEL} : set \rail@y to level LEVEL
+
+\newcount\rail@x
+\newcount\rail@y
+\newcount\rail@ex
+\newcount\rail@sx
+\newcount\rail@rx
+
+\newcount\rail@tmpa
+\newcount\rail@tmpb
+\newcount\rail@tmpc
+
+\def\rail@put{\put(\number\rail@x,\number\rail@y)}
+
+\def\rail@vput{\put(\number\rail@ex,\number\rail@y)}
+
+\def\rail@eline{
+\rail@tmpb=\rail@x
+\advance\rail@tmpb by -\rail@ex
+\rail@put{\line(-1,0){\number\rail@tmpb}}
+}
+
+\def\rail@vreline{
+\rail@tmpb=\rail@x
+\advance\rail@tmpb by -\rail@ex
+\rail@vput{\vector(1,0){\number\rail@tmpb}}
+}
+
+\def\rail@vleline{
+\rail@tmpb=\rail@x
+\advance\rail@tmpb by -\rail@ex
+\rail@put{\vector(-1,0){\number\rail@tmpb}}
+}
+
+\def\rail@sety#1{
+\rail@y=#1
+\multiply\rail@y by -\rail@boxsp
+\advance\rail@y by -\rail@boxht
+}
+
+% \rail@begin{HEIGHT}{NAME} : begin a railroad diagram of height HEIGHT
+%
+% \rail@end : end a railroad diagram
+%
+% \rail@expand{IDENT} : expand IDENT
+
+\def\rail@begin#1#2{
+\item
+\begin{minipage}[t]{\linewidth}
+\ifx\@empty#2\else
+{\rail@namefont \rail@expand{#2}}\\*[\railnamesep]
+\fi
+\unitlength=\railunit
+\rail@tmpa=#1
+\multiply\rail@tmpa by \rail@boxsp
+\begin{picture}(0,\number\rail@tmpa)(0,-\number\rail@tmpa)
+\rail@ex=0
+\rail@rx=0
+\rail@x=\rail@extra
+\rail@sx=\rail@x
+\rail@sety{0}
+}
+
+\def\rail@end{
+\advance\rail@x by \rail@extra
+\rail@eline
+\end{picture}
+\end{minipage}
+}
+
+\def\rail@vend{
+\advance\rail@x by \rail@extra
+\rail@vreline
+\end{picture}
+\end{minipage}
+}
+
+\def\rail@expand#1{\@ifundefined{rail@t@#1}{#1}{\csname rail@t@#1\endcsname}}
+
+% \rail@token{TEXT}[ANNOT] : format token TEXT with annotation
+% \rail@ltoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow left
+% \rail@rtoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow right
+%
+% \rail@ctoken{TEXT}[ANNOT] : format token TEXT centered with annotation
+% \rail@lctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow left
+% \rail@rctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow right
+%
+% \rail@nont{TEXT}[ANNOT] : format nonterminal TEXT with annotation
+% \rail@lnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation, arrow left
+% \rail@rnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation. arrow right
+%
+% \rail@cnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation
+% \rail@lcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
+%                             arrow left
+% \rail@rcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
+%                             arrow right
+%
+% \rail@term{TEXT}[ANNOT] : format terminal TEXT with annotation
+% \rail@lterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow left
+% \rail@rterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow right
+%
+% \rail@cterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation
+% \rail@lcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation, arrow left
+% \rail@rcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation,
+%                             arrow right
+%
+% \rail@annote[TEXT] : format TEXT as annotation
+
+\def\rail@token#1[#2]{
+\rail@setbox{%
+{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@oval
+}
+
+\def\rail@ltoken#1[#2]{
+\rail@setbox{%
+{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vloval
+}
+
+\def\rail@rtoken#1[#2]{
+\rail@setbox{%
+{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vroval
+}
+
+\def\rail@ctoken#1[#2]{
+\rail@setbox{%
+{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@coval
+}
+
+\def\rail@lctoken#1[#2]{
+\rail@setbox{%
+{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vlcoval
+}
+
+\def\rail@rctoken#1[#2]{
+\rail@setbox{%
+{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vrcoval
+}
+
+\def\rail@nont#1[#2]{
+\rail@setbox{%
+{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@frame
+}
+
+\def\rail@lnont#1[#2]{
+\rail@setbox{%
+{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vlframe
+}
+
+\def\rail@rnont#1[#2]{
+\rail@setbox{%
+{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vrframe
+}
+
+\def\rail@cnont#1[#2]{
+\rail@setbox{%
+{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@cframe
+}
+
+\def\rail@lcnont#1[#2]{
+\rail@setbox{%
+{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vlcframe
+}
+
+\def\rail@rcnont#1[#2]{
+\rail@setbox{%
+{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vrcframe
+}
+
+\def\rail@term#1[#2]{
+\rail@setbox{%
+{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@oval
+}
+
+\def\rail@lterm#1[#2]{
+\rail@setbox{%
+{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vloval
+}
+
+\def\rail@rterm#1[#2]{
+\rail@setbox{%
+{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vroval
+}
+
+\def\rail@cterm#1[#2]{
+\rail@setbox{%
+{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@coval
+}
+
+\def\rail@lcterm#1[#2]{
+\rail@setbox{%
+{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vlcoval
+}
+
+\def\rail@rcterm#1[#2]{
+\rail@setbox{%
+{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
+}
+\rail@vrcoval
+}
+
+\def\rail@annote[#1]{
+\rail@setbox{\rail@annofont #1}
+\rail@text
+}
+
+% \rail@box : temporary box for \rail@oval and \rail@frame
+%
+% \rail@setbox{TEXT} : set \rail@box to TEXT, set \rail@tmpa to width
+%
+% \rail@oval : format \rail@box of width \rail@tmpa inside an oval
+% \rail@vloval : format \rail@box of width \rail@tmpa inside an oval, vector left
+% \rail@vroval : format \rail@box of width \rail@tmpa inside an oval, vector right
+%
+% \rail@coval : same as \rail@oval, but centered between \rail@x and
+%               \rail@mx
+% \rail@vlcoval : same as \rail@oval, but centered between \rail@x and
+%                 \rail@mx, vector left
+% \rail@vrcoval : same as \rail@oval, but centered between \rail@x and
+%                 \rail@mx, vector right
+%
+% \rail@frame : format \rail@box of width \rail@tmpa inside a frame
+% \rail@vlframe : format \rail@box of width \rail@tmpa inside a frame, vector left
+% \rail@vrframe : format \rail@box of width \rail@tmpa inside a frame, vector right
+%
+% \rail@cframe : same as \rail@frame, but centered between \rail@x and
+%                \rail@mx
+% \rail@vlcframe : same as \rail@frame, but centered between \rail@x and
+%                  \rail@mx, vector left
+% \rail@vrcframe : same as \rail@frame, but centered between \rail@x and
+%                  \rail@mx, vector right
+%
+% \rail@text : format \rail@box of width \rail@tmpa above the line
+
+\newbox\rail@box
+
+\def\rail@setbox#1{
+\setbox\rail@box\hbox{\strut#1}
+\rail@tmpa=\wd\rail@box
+\divide\rail@tmpa by \railunit
+}
+
+\def\rail@oval{
+\advance\rail@x by \rail@boxlf
+\rail@eline
+\advance\rail@tmpa by \rail@ovalsp
+\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
+\rail@tmpb=\rail@tmpa
+\divide\rail@tmpb by 2
+\advance\rail@y by -\rail@boxhht
+\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
+\advance\rail@y by \rail@boxhht
+\advance\rail@x by \rail@tmpb
+\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
+\advance\rail@x by \rail@tmpb
+\rail@ex=\rail@x
+\advance\rail@x by \rail@boxrt
+}
+
+\def\rail@vloval{
+\advance\rail@x by \rail@boxlf
+\rail@eline
+\advance\rail@tmpa by \rail@ovalsp
+\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
+\rail@tmpb=\rail@tmpa
+\divide\rail@tmpb by 2
+\advance\rail@y by -\rail@boxhht
+\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
+\advance\rail@y by \rail@boxhht
+\advance\rail@x by \rail@tmpb
+\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
+\advance\rail@x by \rail@tmpb
+\rail@ex=\rail@x
+\advance\rail@x by \rail@boxrt
+\rail@vleline
+}
+
+\def\rail@vroval{
+\advance\rail@x by \rail@boxlf
+\rail@vreline
+\advance\rail@tmpa by \rail@ovalsp
+\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
+\rail@tmpb=\rail@tmpa
+\divide\rail@tmpb by 2
+\advance\rail@y by -\rail@boxhht
+\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
+\advance\rail@y by \rail@boxhht
+\advance\rail@x by \rail@tmpb
+\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
+\advance\rail@x by \rail@tmpb
+\rail@ex=\rail@x
+\advance\rail@x by \rail@boxrt
+}
+
+\def\rail@coval{
+\rail@tmpb=\rail@tmpa
+\advance\rail@tmpb by \rail@ovalsp
+\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
+\advance\rail@tmpb by \rail@boxlf
+\advance\rail@tmpb by \rail@boxrt
+\rail@tmpc=\rail@mx
+\advance\rail@tmpc by -\rail@x
+\advance\rail@tmpc by -\rail@tmpb
+\divide\rail@tmpc by 2
+\ifnum\rail@tmpc>0
+\advance\rail@x by \rail@tmpc
+\fi
+\rail@oval
+}
+
+\def\rail@vlcoval{
+\rail@tmpb=\rail@tmpa
+\advance\rail@tmpb by \rail@ovalsp
+\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
+\advance\rail@tmpb by \rail@boxlf
+\advance\rail@tmpb by \rail@boxrt
+\rail@tmpc=\rail@mx
+\advance\rail@tmpc by -\rail@x
+\advance\rail@tmpc by -\rail@tmpb
+\divide\rail@tmpc by 2
+\ifnum\rail@tmpc>0
+\advance\rail@x by \rail@tmpc
+\fi
+\rail@vloval
+}
+
+\def\rail@vrcoval{
+\rail@tmpb=\rail@tmpa
+\advance\rail@tmpb by \rail@ovalsp
+\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
+\advance\rail@tmpb by \rail@boxlf
+\advance\rail@tmpb by \rail@boxrt
+\rail@tmpc=\rail@mx
+\advance\rail@tmpc by -\rail@x
+\advance\rail@tmpc by -\rail@tmpb
+\divide\rail@tmpc by 2
+\ifnum\rail@tmpc>0
+\advance\rail@x by \rail@tmpc
+\fi
+\rail@vroval
+}
+
+\def\rail@frame{
+\advance\rail@x by \rail@boxlf
+\rail@eline
+\advance\rail@tmpa by \rail@framesp
+\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
+\advance\rail@y by -\rail@boxhht
+\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
+\advance\rail@y by \rail@boxhht
+\advance\rail@x by \rail@tmpa
+\rail@ex=\rail@x
+\advance\rail@x by \rail@boxrt
+}
+
+\def\rail@vlframe{
+\advance\rail@x by \rail@boxlf
+\rail@eline
+\advance\rail@tmpa by \rail@framesp
+\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
+\advance\rail@y by -\rail@boxhht
+\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
+\advance\rail@y by \rail@boxhht
+\advance\rail@x by \rail@tmpa
+\rail@ex=\rail@x
+\advance\rail@x by \rail@boxrt
+\rail@vleline
+}
+
+\def\rail@vrframe{
+\advance\rail@x by \rail@boxlf
+\rail@vreline
+\advance\rail@tmpa by \rail@framesp
+\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
+\advance\rail@y by -\rail@boxhht
+\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
+\advance\rail@y by \rail@boxhht
+\advance\rail@x by \rail@tmpa
+\rail@ex=\rail@x
+\advance\rail@x by \rail@boxrt
+}
+
+\def\rail@cframe{
+\rail@tmpb=\rail@tmpa
+\advance\rail@tmpb by \rail@framesp
+\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
+\advance\rail@tmpb by \rail@boxlf
+\advance\rail@tmpb by \rail@boxrt
+\rail@tmpc=\rail@mx
+\advance\rail@tmpc by -\rail@x
+\advance\rail@tmpc by -\rail@tmpb
+\divide\rail@tmpc by 2
+\ifnum\rail@tmpc>0
+\advance\rail@x by \rail@tmpc
+\fi
+\rail@frame
+}
+
+\def\rail@vlcframe{
+\rail@tmpb=\rail@tmpa
+\advance\rail@tmpb by \rail@framesp
+\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
+\advance\rail@tmpb by \rail@boxlf
+\advance\rail@tmpb by \rail@boxrt
+\rail@tmpc=\rail@mx
+\advance\rail@tmpc by -\rail@x
+\advance\rail@tmpc by -\rail@tmpb
+\divide\rail@tmpc by 2
+\ifnum\rail@tmpc>0
+\advance\rail@x by \rail@tmpc
+\fi
+\rail@vlframe
+}
+
+\def\rail@vrcframe{
+\rail@tmpb=\rail@tmpa
+\advance\rail@tmpb by \rail@framesp
+\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
+\advance\rail@tmpb by \rail@boxlf
+\advance\rail@tmpb by \rail@boxrt
+\rail@tmpc=\rail@mx
+\advance\rail@tmpc by -\rail@x
+\advance\rail@tmpc by -\rail@tmpb
+\divide\rail@tmpc by 2
+\ifnum\rail@tmpc>0
+\advance\rail@x by \rail@tmpc
+\fi
+\rail@vrframe
+}
+
+\def\rail@text{
+\advance\rail@x by \rail@textlf
+\advance\rail@y by \rail@textup
+\rail@put{\box\rail@box}
+\advance\rail@y by -\rail@textup
+\advance\rail@x by \rail@tmpa
+\advance\rail@x by \rail@textrt
+}
+
+% alternatives
+%
+% \rail@jx \rail@jy : current join point
+%
+% \rail@gx \rail@gy \rail@gex \rail@grx : global versions of \rail@x etc,
+%                                         to pass values over group closings
+%
+% \rail@mx : maximum x so far
+%
+% \rail@sy : starting \rail@y for alternatives
+%
+% \rail@jput : put at (\rail@jx,\rail@jy)
+%
+% \rail@joval[PART] : put \oval[PART] with adjust
+
+\newcount\rail@jx
+\newcount\rail@jy
+
+\newcount\rail@gx
+\newcount\rail@gy
+\newcount\rail@gex
+\newcount\rail@grx
+
+\newcount\rail@sy
+\newcount\rail@mx
+
+\def\rail@jput{
+\put(\number\rail@jx,\number\rail@jy)
+}
+
+\def\rail@joval[#1]{
+\advance\rail@jx by \rail@joinadj
+\rail@jput{\oval(\number\rail@joinsz,\number\rail@joinsz)[#1]}
+\advance\rail@jx by -\rail@joinadj
+}
+
+% \rail@barsplit : incoming split for '|'
+%
+% \rail@plussplit : incoming split for '+'
+%
+
+\def\rail@barsplit{
+\advance\rail@jy by -\rail@joinhsz
+\rail@joval[tr]
+\advance\rail@jx by \rail@joinhsz
+}
+
+\def\rail@plussplit{
+\advance\rail@jy by -\rail@joinhsz
+\advance\rail@jx by \rail@joinsz
+\rail@joval[tl]
+\advance\rail@jx by -\rail@joinhsz
+}
+
+% \rail@alt{SPLIT} : start alternatives with incoming split SPLIT
+%
+
+\def\rail@alt#1{
+\rail@sy=\rail@y
+\rail@jx=\rail@x
+\rail@jy=\rail@y
+\advance\rail@x by \rail@joinsz
+\rail@mx=0
+\let\rail@list=\@empty
+\let\rail@comma=\@empty
+\let\rail@split=#1
+\begingroup
+\rail@sx=\rail@x
+\rail@rx=0
+}
+
+% \rail@nextalt{FIX}{Y} : start next alternative at vertical position Y
+%                         and fix-up FIX
+%
+
+\def\rail@nextalt#1#2{
+\global\rail@gx=\rail@x
+\global\rail@gy=\rail@y
+\global\rail@gex=\rail@ex
+\global\rail@grx=\rail@rx
+\endgroup
+#1
+\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
+\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
+\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
+\def\rail@comma{,}
+\rail@split
+\let\rail@split=\@empty
+\rail@sety{#2}
+\rail@tmpa=\rail@jy
+\advance\rail@tmpa by -\rail@y
+\advance\rail@tmpa by -\rail@joinhsz
+\rail@jput{\line(0,-1){\number\rail@tmpa}}
+\rail@jy=\rail@y
+\advance\rail@jy by \rail@joinhsz
+\advance\rail@jx by \rail@joinhsz
+\rail@joval[bl]
+\advance\rail@jx by -\rail@joinhsz
+\rail@ex=\rail@x
+\begingroup
+\rail@sx=\rail@x
+\rail@rx=0
+}
+
+% \rail@barjoin : outgoing join for first '|' alternative
+%
+% \rail@plusjoin : outgoing join for first '+' alternative
+%
+% \rail@altjoin : join for subsequent alternative
+%
+
+\def\rail@barjoin{
+\ifnum\rail@y<\rail@sy
+\global\rail@gex=\rail@jx
+\else
+\global\rail@gex=\rail@ex
+\fi
+\advance\rail@jy by -\rail@joinhsz
+\rail@joval[tl]
+\advance\rail@jx by -\rail@joinhsz
+\ifnum\rail@y<\rail@sy
+\rail@altjoin
+\fi
+}
+
+\def\rail@plusjoin{
+\global\rail@gex=\rail@ex
+\advance\rail@jy by -\rail@joinhsz
+\advance\rail@jx by -\rail@joinsz
+\rail@joval[tr]
+\advance\rail@jx by \rail@joinhsz
+}
+
+\def\rail@altjoin{
+\rail@eline
+\rail@tmpa=\rail@jy
+\advance\rail@tmpa by -\rail@y
+\advance\rail@tmpa by -\rail@joinhsz
+\rail@jput{\line(0,-1){\number\rail@tmpa}}
+\rail@jy=\rail@y
+\advance\rail@jy by \rail@joinhsz
+\advance\rail@jx by -\rail@joinhsz
+\rail@joval[br]
+\advance\rail@jx by \rail@joinhsz
+}
+
+% \rail@eltsplit EX:Y; : split EX:Y into \rail@ex \rail@y
+%
+% \rail@endalt{JOIN} : end alternatives with outgoing join JOIN
+
+\def\rail@eltsplit#1:#2;{\rail@ex=#1\rail@y=#2}
+
+\def\rail@endalt#1{
+\global\rail@gx=\rail@x
+\global\rail@gy=\rail@y
+\global\rail@gex=\rail@ex
+\global\rail@grx=\rail@rx
+\endgroup
+\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
+\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
+\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
+\rail@x=\rail@mx
+\rail@jx=\rail@x
+\rail@jy=\rail@sy
+\advance\rail@jx by \rail@joinsz
+\let\rail@join=#1
+\@for\rail@elt:=\rail@list\do{
+\expandafter\rail@eltsplit\rail@elt;
+\rail@join
+\let\rail@join=\rail@altjoin
+}
+\rail@x=\rail@mx
+\rail@y=\rail@sy
+\rail@ex=\rail@gex
+\advance\rail@x by \rail@joinsz
+}
+
+% \rail@bar : start '|' alternatives
+%
+% \rail@nextbar : next '|' alternative
+%
+% \rail@endbar : end '|' alternatives
+%
+
+\def\rail@bar{
+\rail@alt\rail@barsplit
+}
+
+\def\rail@nextbar{
+\rail@nextalt\relax
+}
+
+\def\rail@endbar{
+\rail@endalt\rail@barjoin
+}
+
+% \rail@plus : start '+' alternatives
+%
+% \rail@nextplus: next '+' alternative
+%
+% \rail@endplus : end '+' alternatives
+%
+
+\def\rail@plus{
+\rail@alt\rail@plussplit
+}
+
+\def\rail@nextplus{
+\rail@nextalt\rail@fixplus
+}
+
+\def\rail@fixplus{
+\ifnum\rail@gy<\rail@sy
+\begingroup
+\rail@x=\rail@gx
+\rail@y=\rail@gy
+\rail@ex=\rail@gex
+\rail@rx=\rail@grx
+\ifnum\rail@x<\rail@rx
+\rail@x=\rail@rx
+\fi
+\rail@eline
+\rail@jx=\rail@x
+\rail@jy=\rail@y
+\advance\rail@jy by \rail@joinhsz
+\rail@joval[br]
+\advance\rail@jx by \rail@joinhsz
+\rail@tmpa=\rail@sy
+\advance\rail@tmpa by -\rail@joinhsz
+\advance\rail@tmpa by -\rail@jy
+\rail@jput{\line(0,1){\number\rail@tmpa}}
+\rail@jy=\rail@sy
+\advance\rail@jy by -\rail@joinhsz
+\advance\rail@jx by \rail@joinhsz
+\rail@joval[tl]
+\advance\rail@jy by \rail@joinhsz
+\global\rail@gx=\rail@jx
+\global\rail@gy=\rail@jy
+\global\rail@gex=\rail@gx
+\global\rail@grx=\rail@rx
+\endgroup
+\fi
+}
+
+\def\rail@endplus{
+\rail@endalt\rail@plusjoin
+}
+
+% \rail@cr{Y} : carriage return to vertical position Y
+
+\def\rail@cr#1{
+\rail@tmpa=\rail@sx
+\advance\rail@tmpa by \rail@joinsz
+\ifnum\rail@x<\rail@tmpa\rail@x=\rail@tmpa\fi
+\rail@eline
+\rail@jx=\rail@x
+\rail@jy=\rail@y
+\advance\rail@x by \rail@joinsz
+\ifnum\rail@x>\rail@rx\rail@rx=\rail@x\fi
+\advance\rail@jy by -\rail@joinhsz
+\rail@joval[tr]
+\advance\rail@jx by \rail@joinhsz
+\rail@sety{#1}
+\rail@tmpa=\rail@jy
+\advance\rail@tmpa by -\rail@y
+\advance\rail@tmpa by -\rail@boxsp
+\advance\rail@tmpa by -\rail@joinhsz
+\rail@jput{\line(0,-1){\number\rail@tmpa}}
+\rail@jy=\rail@y
+\advance\rail@jy by \rail@boxsp
+\advance\rail@jy by \rail@joinhsz
+\advance\rail@jx by -\rail@joinhsz
+\rail@joval[br]
+\advance\rail@jy by -\rail@joinhsz
+\rail@tmpa=\rail@jx
+\advance\rail@tmpa by -\rail@sx
+\advance\rail@tmpa by -\rail@joinhsz
+\rail@jput{\line(-1,0){\number\rail@tmpa}}
+\rail@jx=\rail@sx
+\advance\rail@jx by \rail@joinhsz
+\advance\rail@jy by -\rail@joinhsz
+\rail@joval[tl]
+\advance\rail@jx by -\rail@joinhsz
+\rail@tmpa=\rail@boxsp
+\advance\rail@tmpa by -\rail@joinsz
+\rail@jput{\line(0,-1){\number\rail@tmpa}}
+\advance\rail@jy by -\rail@tmpa
+\advance\rail@jx by \rail@joinhsz
+\rail@joval[bl]
+\rail@x=\rail@jx
+\rail@ex=\rail@x
+}
+
+% default setup for Isabelle
+\newenvironment{railoutput}%
+{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\makeatother\end{list}}
+
+\def\rail@termfont{\isabellestyle{tt}}
+\def\rail@nontfont{\isabellestyle{it}}
+\def\rail@namefont{\isabellestyle{it}}
diff -r fac2f374d001 -r 168abe8dd1e3 src/Tools/isac/ROOT
--- a/src/Tools/isac/ROOT	Tue Mar 10 13:25:00 2020 +0100
+++ b/src/Tools/isac/ROOT	Wed Mar 11 15:25:52 2020 +0100
@@ -26,7 +26,7 @@
     Build_Isac
 
 (* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
-session Lucas_Interpreter = HOL +
+session Interpret = HOL +
   description \<open>
     Session Isac restricted to code required for Lucas_Interpreter.
     "Lucas-Interpretation on Isabelle’s Functions"