1.1 --- a/doc-isac/mat-eng-en.tex	Wed Nov 29 07:51:28 2023 +0100
     1.2 +++ b/doc-isac/mat-eng-en.tex	Thu Nov 30 08:11:50 2023 +0100
     1.3 @@ -1008,10 +1008,10 @@
     1.4  \end{verbatim}}%size
     1.5  Given a formalization (and a specification of the problem, i.e. a theory, a problemtype, and a method) \isac{} can solve the respective problem automatically. The formalization must match the problem type for this purpose:
     1.6  {\footnotesize\begin{verbatim}
     1.7 -   ML> match_pbl;
     1.8 +   ML> by_formalise;
     1.9     val it = fn : fmz -> pbt -> match'
    1.10     ML>
    1.11 -   ML> match_pbl fmz (get_pbt ["univariate","equation"]);
    1.12 +   ML> by_formalise fmz (get_pbt ["univariate","equation"]);
    1.13     val it =
    1.14       Matches'
    1.15         {Find=[Correct "solutions L"],
    1.16 @@ -1019,7 +1019,7 @@
    1.17          Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]}
    1.18       : match'
    1.19     ML>
    1.20 -   ML> match_pbl fmz (get_pbt ["linear","univariate","equation"]);
    1.21 +   ML> by_formalise fmz (get_pbt ["linear","univariate","equation"]);
    1.22     val it =
    1.23       Matches'
    1.24         {Find=[Correct "solutions L"],
    1.25 @@ -1032,7 +1032,7 @@
    1.26                    matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"],
    1.27          With=[]} : match'
    1.28     ML>
    1.29 -   ML> match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
    1.30 +   ML> by_formalise fmz (get_pbt ["squareroot","univariate","equation"]);
    1.31     val it =
    1.32       NoMatch'
    1.33         {Find=[Correct "solutions L"],