1.1 --- a/doc-isac/mat-eng-de.tex	Sun Oct 09 07:44:22 2022 +0200
     1.2 +++ b/doc-isac/mat-eng-de.tex	Sun Oct 09 09:01:29 2022 +0200
     1.3 @@ -70,9 +70,9 @@
     1.4     > "a + b * 3";
     1.5        val it = "a + b * 3" : string
     1.6  \end{verbatim}}
     1.7 -\noindent ``a + b * 3'' ist also ein string (eine Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"ur Formeln. In diese kann man mit der Funktion {\tt str2term} (string to term) umrechnen:
     1.8 +\noindent ``a + b * 3'' ist also ein string (eine Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"ur Formeln. In diese kann man mit der Funktion {\tt TermC.parse_test @{context}} (string to term) umrechnen:
     1.9  {\footnotesize\begin{verbatim}
    1.10 -   > str2term "a + b * 3";
    1.11 +   > TermC.parse_test @{context} "a + b * 3";
    1.12        val it =
    1.13           Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
    1.14                 Free ("a", "RealDef.real") $
    1.15 @@ -81,7 +81,7 @@
    1.16  \end{verbatim}}
    1.17  \noindent Diese Form heisst {\tt term} und ist nicht f\"ur den Menschen zum lesen gedacht. Isabelle braucht sie aber intern zum Rechnen. Wir wollen sie mit Hilfe von {\tt val} (value) auf der Variable {\tt t} speichern:
    1.18  {\footnotesize\begin{verbatim}
    1.19 -   > val t = str2term "a + b * 3";
    1.20 +   > val t = TermC.parse_test @{context} "a + b * 3";
    1.21        val t =  
    1.22           Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
    1.23                 Free ("a", "RealDef.real") $
    1.24 @@ -154,7 +154,7 @@
    1.25  
    1.26  Wollen Sie wissen, wie die einzelnen Rechengesetze aussehen, k\"onnen Sie im Internet folgenden Link ansehen: http://isabelle.in.tum.de/dist/library/HOL/Groups.html
    1.27  
    1.28 -\paragraph{} Der Vorgang, bei dem aus einem {\tt string} ein Term entsteht, nennt man Parsing. Dazu wird Wissen aus der Theorie ben\"otigt, denn {\tt str2term} nimmt intern eine parse-Funktion, bei der immer das gesamte \isac{}-Wissen verwendet wird. Bei dieser Funktion wird weiters festgelegt, aus welcher Theorie das Wissen genommen werden soll.
    1.29 +\paragraph{} Der Vorgang, bei dem aus einem {\tt string} ein Term entsteht, nennt man Parsing. Dazu wird Wissen aus der Theorie ben\"otigt, denn {\tt TermC.parse_test @{context}} nimmt intern eine parse-Funktion, bei der immer das gesamte \isac{}-Wissen verwendet wird. Bei dieser Funktion wird weiters festgelegt, aus welcher Theorie das Wissen genommen werden soll.
    1.30  {\footnotesize\begin{verbatim}
    1.31     > parse Isac.thy "a + b";
    1.32        val it = Some "a + b" : Thm.cterm Library.option