1.1 --- a/doc-isac/mat-eng-de.tex	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/doc-isac/mat-eng-de.tex	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -338,7 +338,7 @@
     1.4        val it = fn
     1.5        :
     1.6        theory' ->
     1.7 -      rew_ord' ->
     1.8 +      rew_ord ->
     1.9        rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
    1.10  \end{verbatim}}
    1.11  Die Funktion hat zwei Argumente, die mitgeschickt werden m\"ussen, damit die Funktion arbeiten kann. Das letzte Element {\tt (cterm' * cterm' list) Library.option} im unteren Term ist das Ergebnis, das die Funktionen {\tt rewrite} zur\"uckgeben und die zwei vorhergehenden Argumente, {\tt theorem} und {\tt cterm}, sind die f\"ur uns wichtigen. {\tt Theorem} ist die Rechenregel und {\tt cterm} jene Formel auf die die Rechenregel angewendet wird.
    1.12 @@ -347,7 +347,7 @@
    1.13        val it = fn
    1.14        :
    1.15        theory' ->
    1.16 -      rew_ord' ->
    1.17 +      rew_ord ->
    1.18        rls' ->bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option
    1.19  \end{verbatim}}
    1.20  Die Funktion {\tt rewrite\_inst} wird ben\"otigt, um Gleichungen, Rechnungen zum Differenzieren etc. zu l\"osen. Dabei wird die gebundene Variable (bdv) instanziiert, d.h. es wird die Variable angegeben, nach der man differenzieren will, bzw. f\"ur die ein Wert bei einer Gleichung herauskommen soll.
    1.21 @@ -436,25 +436,25 @@
    1.22        val it =
    1.23           Rls
    1.24              {id = "rearrange_assoc",
    1.25 -               scr = Script (Free ("empty_script", "RealDef.real")),
    1.26 +               program = Script (Free ("empty_script", "RealDef.real")),
    1.27                 calc = [],
    1.28 -               erls =
    1.29 +               asm_rls =
    1.30                 Rls
    1.31                    {id = "e_rls",
    1.32 -                     scr = EmptyScr,
    1.33 +                     program = EmptyScr,
    1.34                       calc = [],
    1.35 -                     erls = Erls,
    1.36 -                     srls = Erls,
    1.37 +                     asm_rls = Erls,
    1.38 +                     prog_rls = Erls,
    1.39                       rules = [],
    1.40                       rew_ord = ("dummy_ord", fn),
    1.41                       preconds = []},
    1.42 -               srls =
    1.43 +               prog_rls =
    1.44                 Rls
    1.45                    {id = "e_rls",
    1.46 -                     scr = EmptyScr,
    1.47 +                     program = EmptyScr,
    1.48                       calc = [],
    1.49 -                     erls = Erls,
    1.50 -                     srls = Erls,
    1.51 +                     asm_rls = Erls,
    1.52 +                     prog_rls = Erls,
    1.53                       rules = [],
    1.54                       rew_ord = ("dummy_ord", fn),
    1.55                       preconds = []},
    1.56 @@ -1112,7 +1112,7 @@
    1.57  {\it fmz}
    1.58  & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\
    1.59  {\it met}
    1.60 -& eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\
    1.61 +& eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it program}, etc.)\\
    1.62  {\it metID}
    1.63  & bezieht sich auf {\it met}\\
    1.64  {\it op}
    1.65 @@ -1127,7 +1127,7 @@
    1.66  & rule set, d.h. eine Datenstruktur, die theorems {\it thm} und Operatoren {\it op} zur Vereinfachung (mit {\it rew\_ord}) enth\"alt \\
    1.67  {\it Rrls}
    1.68  & rule set f\"ur das 'reverse rewriting' (eine \isac-Technik, die schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\
    1.69 -{\it scr}
    1.70 +{\it program}
    1.71  & script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\
    1.72  {\it norm\_rls}
    1.73  & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\
    1.74 @@ -1154,7 +1154,7 @@
    1.75  \begin{center}
    1.76  \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
    1.77  tactic &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
    1.78 -& &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
    1.79 +& &thy &program &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
    1.80  \hline\hline
    1.81  Init\_Proof
    1.82  &fmz & x & & & x & & & & & & & x \\