doc-src/isac/mlehnfeld/projektbericht.tex
branchdecompose-isar
changeset 42037 ee2c2928150e
parent 42036 145514dbfb57
child 42038 59b7fd45b037
     1.1 --- a/doc-src/isac/mlehnfeld/projektbericht.tex	Mon May 30 02:04:29 2011 +0200
     1.2 +++ b/doc-src/isac/mlehnfeld/projektbericht.tex	Mon May 30 11:02:21 2011 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  \>\>{fun init \_} = []);\\
     1.5  \\
     1.6  fun insert\_assumptions asms = \\
     1.7 -\>\>\>ContextData{.map} (fn xs => distinct (data@xs));\\
     1.8 +\>\>\>ContextData{.map} (fn xs => distinct (asms@xs));\\
     1.9  \\
    1.10  fun get\_assumptions ctxt = ContextData{.get} ctxt;\\
    1.11  \\
    1.12 @@ -298,7 +298,7 @@
    1.13  \paragraph{Bearbeitung eines Subproblems}~\\
    1.14  
    1.15  Einige Ausführungsschritte später startet der Interpreter mit der Gleichung $-1 + x = 0$ ein Subproblem, beginnt dort wiederum mit Spezifikationsphase und setzt mit der Lösungsphase fort.\\
    1.16 -In einem Zwischenschritt bestehen die lokalen Assumptions aus der Annahme, dass die Gleichung mit der Gleichheitsregel zu matchen ist:\\
    1.17 +In einem Zwischenschritt bestehen die lokalen Assumptions aus der Annahme, dass die Gleichung mit der Gleichheitsregel zu matchen ist:
    1.18  \begin{verbatim}
    1.19  ["matches (?a = ?b) (-1 + x = 0)"]: string list
    1.20  \end{verbatim}