1.1 --- a/doc-isac/mat-eng-en.tex	Thu Dec 22 11:12:18 2016 +0100
     1.2 +++ b/doc-isac/mat-eng-en.tex	Thu Dec 22 11:36:20 2016 +0100
     1.3 @@ -1245,7 +1245,7 @@
     1.4  
     1.5  
     1.6  \section{Initialize the calculation}
     1.7 -The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ptree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons.
     1.8 +The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ctree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons.
     1.9  {\footnotesize\begin{verbatim}
    1.10     ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
    1.11     val mID = "Init_Proof" : string
    1.12 @@ -1263,9 +1263,9 @@
    1.13       Nd
    1.14         (PblObj
    1.15            {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
    1.16 -           result=#,spec=#},[]) : ptree
    1.17 +           result=#,spec=#},[]) : ctree
    1.18     \end{verbatim}}%size
    1.19 -The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ptree}, {\tt pos'}).
    1.20 +The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ctree}, {\tt pos'}).
    1.21  
    1.22  We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
    1.23  {\footnotesize\begin{verbatim}
    1.24 @@ -1347,7 +1347,7 @@
    1.25       Nd
    1.26         (PblObj
    1.27            {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
    1.28 -              result=#,spec=#},[]) : ptree
    1.29 +              result=#,spec=#},[]) : ctree
    1.30  \end{verbatim}}%size
    1.31  The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows.
    1.32  {\footnotesize\begin{verbatim}