diff -r a474900d5bd2 -r 255c853ea2f0 doc-isac/mat-eng-en.tex
--- a/doc-isac/mat-eng-en.tex	Thu Dec 22 11:12:18 2016 +0100
+++ b/doc-isac/mat-eng-en.tex	Thu Dec 22 11:36:20 2016 +0100
@@ -1245,7 +1245,7 @@
 
 
 \section{Initialize the calculation}
-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.
+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.
 {\footnotesize\begin{verbatim}
    ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
    val mID = "Init_Proof" : string
@@ -1263,9 +1263,9 @@
      Nd
        (PblObj
           {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
-           result=#,spec=#},[]) : ptree
+           result=#,spec=#},[]) : ctree
    \end{verbatim}}%size
-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'}).
+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'}).
 
 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
 {\footnotesize\begin{verbatim}
@@ -1347,7 +1347,7 @@
      Nd
        (PblObj
           {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
-              result=#,spec=#},[]) : ptree
+              result=#,spec=#},[]) : ctree
 \end{verbatim}}%size
 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.
 {\footnotesize\begin{verbatim}