1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 19:05:02 2012 +0200
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 19:42:39 2012 +0200
     1.3 @@ -423,17 +423,12 @@
     1.4  The tactics play a specific role in
     1.5  Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
     1.6  break-points where, as a side-effect, a line is added to a calculation
     1.7 -
     1.8 -.\\.\\.\\
     1.9 -
    1.10 -protocol
    1.11 -
    1.12 -.\\.\\.\\
    1.13 -
    1.14 -and control is handed over to the user. The user is free
    1.15 -to investigate underlying knowledge, applicable theorems, etc.  And
    1.16 -the user can proceed constructing a solution by input of a tactic to
    1.17 -be applied or by input of a formula; in the latter case the
    1.18 +as a protocol for proceeding towards a solution in step-wise problem
    1.19 +solving. At the same points Lucas-Interpretation serves interactive
    1.20 +tutoring and control is handed over to the user. The user is free to
    1.21 +investigate underlying knowledge, applicable theorems, etc.  And the
    1.22 +user can proceed constructing a solution by input of a tactic to be
    1.23 +applied or by input of a formula; in the latter case the
    1.24  Lucas-Interpreter has built up a logical context (initialised with the
    1.25  precondition of the formal specification) such that Isabelle can
    1.26  derive the formula from this context --- or give feedback, that no
    1.27 @@ -451,23 +446,28 @@
    1.28  
    1.29  \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
    1.30  if {\it tactic} is applicable, then it is applied to {\it term},
    1.31 -otherwise {\it term} is passed on unchanged.
    1.32 +otherwise {\it term} is passed on without changes.
    1.33  
    1.34  \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
    1.35 -term}\Rightarrow{\it term}$:
    1.36 -
    1.37 +term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
    1.38 +it is applied to the first {\it term} yielding another {\it term},
    1.39 +otherwise the second {\it tactic} is applied; if none is applicable an
    1.40 +exception is raised.
    1.41  
    1.42  \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
    1.43 -term}\Rightarrow{\it term}$:
    1.44 +term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
    1.45 +first {\it term} yielding an intermediate term (not appearing in the
    1.46 +signature) to which the second {\it tactic} is applied.
    1.47  
    1.48  \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
    1.49 -term}\Rightarrow{\it term}$:
    1.50 -
    1.51 +term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
    1.52 +{\it tactic} is applied to the first {\it term} yielding an
    1.53 +intermediate term (not appearing in the signature); the intermediate
    1.54 +term is added to the environment the first {\it term} is evaluated in
    1.55 +etc as long as the first {\it term} is true.
    1.56  \end{description}
    1.57 -
    1.58 -no input / output --- Lucas-Interpretation
    1.59 -
    1.60 -.\\.\\.\\TODO\\.\\.\\
    1.61 +The tacticals are not treated as break-points by Lucas-Interpretation
    1.62 +and thus do not contribute to the calculation nor to interaction.
    1.63  
    1.64  \section{Development of a Program on Trial}\label{trial} 
    1.65  As mentioned above, {\sisac} is an experimental system for a proof of
    1.66 @@ -696,7 +696,7 @@
    1.67  starts with a formal {\em specification} of the problem to be solved.
    1.68  \begin{figure}
    1.69    \begin{center}
    1.70 -    \includegraphics{fig/universe}
    1.71 +    \includegraphics[width=110mm]{fig/math-universe-small}
    1.72      \caption{Didactic ``Math-Universe'': Algorithmic Knowledge
    1.73  (Programs) is combined with Application-oriented Knowledge
    1.74  (Specifications) and Deductive Knowledge (Axioms, Definitions,