1.1 --- a/doc-isac/mat-eng-de.tex	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/doc-isac/mat-eng-de.tex	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -97,9 +97,9 @@
     1.4              (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
     1.5                 ...) : Term.term
     1.6  \end{verbatim}}
     1.7 -Der auf {\tt t} gespeicherte Term kann einer Funktion {\tt atomty} \"ubergeben werden, die diesen in einer dritten Form zeigt:
     1.8 +Der auf {\tt t} gespeicherte Term kann einer Funktion {\tt TermC.atom_trace_detail @{context}} \"ubergeben werden, die diesen in einer dritten Form zeigt:
     1.9  {\footnotesize\begin{verbatim}
    1.10 -   > atomty term;
    1.11 +   > TermC.atom_trace_detail \@\{context\} term;
    1.12   
    1.13     ***
    1.14     *** Const (op +, [real, real] => real)
    1.15 @@ -288,7 +288,7 @@
    1.16           Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
    1.17           Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
    1.18       : Theory.theory
    1.19 -   > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.20 +   > ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.21   
    1.22        ***
    1.23        *** Free (d_d, [real, real] => real)
    1.24 @@ -316,7 +316,7 @@
    1.25           Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
    1.26           PolyEq, LogExp, Diff} : Theory.theory
    1.27   
    1.28 -   > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.29 +   > ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.30   
    1.31        ***
    1.32        *** Const (Diff.d_d, [real, real] => real)
    1.33 @@ -581,11 +581,11 @@
    1.34  "\n"
    1.35  val it = "\n" : string
    1.36  \end{verbatim}}
    1.37 -Das Modell wird durch den Befehl \textit{free2var} erstellt.
    1.38 +Das Modell wird durch den Befehl \textit{mk_Var} erstellt.
    1.39  {\footnotesize\begin{verbatim}
    1.40 -> free2var;
    1.41 +> mk_Var;
    1.42  val it = fn : Term.term -> Term.term
    1.43 -> val pat = free2var p;
    1.44 +> val pat = mk_Var p;
    1.45  val pat =
    1.46  Const ("op =", "[RealDef.real, RealDef.real] => bool") $
    1.47  (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $