equal
deleted
inserted
replaced
46 \item xxx |
46 \item xxx |
47 \item xxx |
47 \item xxx |
48 \item xxx |
48 \item xxx |
49 \item xxx |
49 \item xxx |
50 \item in check_leaf SEPARATE tracing |
50 \item in check_leaf SEPARATE tracing |
51 collect all trace_script --> Trace_LI |
51 collect all trace_LI --> Trace_LI |
52 trace_script: replace ' by " in writeln |
52 trace_LI: replace ' by " in writeln |
53 \item xxx |
53 \item xxx |
54 \item renamings |
|
55 \begin{itemize} |
|
56 \item xxx |
|
57 \item xxx |
|
58 \item rename field scr in meth |
|
59 \item xxx |
|
60 \item xxx |
|
61 \end{itemize} |
|
62 \item xxx |
54 \item xxx |
63 \item relocations + renamings |
55 \item relocations + renamings |
64 \begin{itemize} |
56 \begin{itemize} |
65 \item Rule.terms2str -> TermC.s_to_string |
57 \item Rule.terms2str -> TermC.s_to_string |
66 Tactic_Def.tac2str -> Tactic_Def.input_to_string |
58 Tactic_Def.tac2str -> Tactic_Def.input_to_string |
136 \item LI.do_next (*TODO RM..*) ??? |
128 \item LI.do_next (*TODO RM..*) ??? |
137 \item generate.sml: RM datatype edit TOGETHER WITH datatype inout |
129 \item generate.sml: RM datatype edit TOGETHER WITH datatype inout |
138 \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ |
130 \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ |
139 \item get_ctxt_LI should replace get_ctxt |
131 \item get_ctxt_LI should replace get_ctxt |
140 \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge |
132 \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge |
141 \item rename Base_Tool.thy <--- Base_Tools |
133 \item rename Base_Tool.thy <--- Base_Tools |
142 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc |
134 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc |
|
135 \item rename field scr in meth |
|
136 \item xxx |
143 \item xxx |
137 \item xxx |
144 \item xxx |
138 \item xxx |
145 \item cleanup fun me: |
139 \item cleanup fun me: |
146 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p) |
140 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p) |
147 | me*) (_, tac) p _(*NEW remove*) pt = |
141 | me*) (_, tac) p _(*NEW remove*) pt = |
253 \item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*) |
247 \item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*) |
254 \item xxx |
248 \item xxx |
255 \item automatically extrac rls from program-code |
249 \item automatically extrac rls from program-code |
256 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ? |
250 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ? |
257 \item xxx |
251 \item xxx |
258 \item finish output of trace_script with Check_Postcond (useful for SubProblem) |
252 \item finish output of trace_LI with Check_Postcond (useful for SubProblem) |
259 \item xxx |
253 \item xxx |
260 \item xxx |
254 \item xxx |
261 \item xxx |
255 \item xxx |
262 \item xxx |
256 \item xxx |
263 \item xxx |
257 \item xxx |