equal
deleted
inserted
replaced
100 structure ContextData = {Proof\_Data}\\ |
100 structure ContextData = {Proof\_Data}\\ |
101 \>~({type T} = term list\\ |
101 \>~({type T} = term list\\ |
102 \>\>{fun init \_} = []);\\ |
102 \>\>{fun init \_} = []);\\ |
103 \\ |
103 \\ |
104 fun insert\_assumptions asms = \\ |
104 fun insert\_assumptions asms = \\ |
105 \>\>\>ContextData{.map} (fn xs => distinct (data@xs));\\ |
105 \>\>\>ContextData{.map} (fn xs => distinct (asms@xs));\\ |
106 \\ |
106 \\ |
107 fun get\_assumptions ctxt = ContextData{.get} ctxt;\\ |
107 fun get\_assumptions ctxt = ContextData{.get} ctxt;\\ |
108 \\ |
108 \\ |
109 \\ |
109 \\ |
110 val declare\_constraints : \\ |
110 val declare\_constraints : \\ |
296 \end{verbatim} |
296 \end{verbatim} |
297 |
297 |
298 \paragraph{Bearbeitung eines Subproblems}~\\ |
298 \paragraph{Bearbeitung eines Subproblems}~\\ |
299 |
299 |
300 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.\\ |
300 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.\\ |
301 In einem Zwischenschritt bestehen die lokalen Assumptions aus der Annahme, dass die Gleichung mit der Gleichheitsregel zu matchen ist:\\ |
301 In einem Zwischenschritt bestehen die lokalen Assumptions aus der Annahme, dass die Gleichung mit der Gleichheitsregel zu matchen ist: |
302 \begin{verbatim} |
302 \begin{verbatim} |
303 ["matches (?a = ?b) (-1 + x = 0)"]: string list |
303 ["matches (?a = ?b) (-1 + x = 0)"]: string list |
304 \end{verbatim} |
304 \end{verbatim} |
305 Nach künstlichem Einfügen zweier Assumptions und Beendigung des Subproblems steht eine Lösung für \textit{x} in den Assumptions:\\ |
305 Nach künstlichem Einfügen zweier Assumptions und Beendigung des Subproblems steht eine Lösung für \textit{x} in den Assumptions:\\ |
306 \texttt{[\dq{}matches (?a = ?b) (-1 + x = 0)\dq{}, \dq{}x < sub\_asm\_out\dq{}, \dq{}{\bf x = 1}\dq{}, \dq{}precond\_rootmet x\dq{}]: string list}\\ |
306 \texttt{[\dq{}matches (?a = ?b) (-1 + x = 0)\dq{}, \dq{}x < sub\_asm\_out\dq{}, \dq{}{\bf x = 1}\dq{}, \dq{}precond\_rootmet x\dq{}]: string list}\\ |