equal
deleted
inserted
replaced
36 \item switch args |
36 \item switch args |
37 check_tac cc ist (form_arg, prog_tac) to |
37 check_tac cc ist (form_arg, prog_tac) to |
38 check_tac cc ist (prog_tac, form_arg) |
38 check_tac cc ist (prog_tac, form_arg) |
39 + in check_tac1 |
39 + in check_tac1 |
40 \item xxx |
40 \item xxx |
41 \item shift check_leaf Lucin --> LucinNEW ? LItool ? |
|
42 \item xxx |
|
43 \item rm test/..--- check Scripts --- |
41 \item rm test/..--- check Scripts --- |
44 \item xxx |
42 \item xxx |
45 \item reformat + rename "fun eval_leaf"+"fun get_stac" |
43 \item reformat + rename "fun eval_leaf"+"fun get_stac" |
46 (*1*)(*2*) |
44 (*1*)(*2*) |
47 ?consistency with subst term? |
45 ?consistency with subst term? |
71 \item xxx |
69 \item xxx |
72 \item distribute test/../scrtools.sml |
70 \item distribute test/../scrtools.sml |
73 \item xxx |
71 \item xxx |
74 \item xxx |
72 \item xxx |
75 \item simplify calls of scan_dn1, scan_dn etc |
73 \item simplify calls of scan_dn1, scan_dn etc |
76 \item open Istate in LucinNEW |
74 \item open Istate in Lucin |
77 \end{itemize} |
75 \end{itemize} |
78 \<close> |
76 \<close> |
79 subsection \<open>Postponed from current changeset\<close> |
77 subsection \<open>Postponed from current changeset\<close> |
80 text \<open> |
78 text \<open> |
81 \begin{itemize} |
79 \begin{itemize} |
169 \item ? what is the difference headline <--> cascmd in |
167 \item ? what is the difference headline <--> cascmd in |
170 Subproblem' (spec, oris, headline, fmz_, context, cascmd) |
168 Subproblem' (spec, oris, headline, fmz_, context, cascmd) |
171 \item xxx |
169 \item xxx |
172 \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr |
170 \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr |
173 \item extract common code from associate.. stac2tac_ |
171 \item extract common code from associate.. stac2tac_ |
174 rename Lucin.stac2tac -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac, |
172 rename LItool.stac2tac -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac, |
175 .. see \<open>Separate ..\<close> |
173 .. see \<open>Separate ..\<close> |
176 \end{itemize} |
174 \end{itemize} |
177 \<close> |
175 \<close> |
178 |
176 |
179 section \<open>Separated tasks\<close> |
177 section \<open>Separated tasks\<close> |
353 \item new: Specify/spec-tac.sml .. Interpret/solve-tac.sml: generate --> insert, etc |
351 \item new: Specify/spec-tac.sml .. Interpret/solve-tac.sml: generate --> insert, etc |
354 \item reduce occurrences of "tactic" in TODO.thy |
352 \item reduce occurrences of "tactic" in TODO.thy |
355 \item xxx |
353 \item xxx |
356 \end{itemize} |
354 \end{itemize} |
357 \item xxx |
355 \item xxx |
358 \item ??????????? WHY CAN LucinNEW.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ??????????? |
356 \item ??????????? WHY CAN Lucin.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ??????????? |
359 \item xxx |
357 \item xxx |
360 \item ..Separate: |
358 \item ..Separate: |
361 MathEngine.solve, ..., |
359 MathEngine.solve, ..., |
362 ? or identify "layers" like in Isabelle? |
360 ? or identify "layers" like in Isabelle? |
363 \item xxx |
361 \item xxx |
441 \item theory can be retrieved from ctxt by Proof_Context.theory_of |
439 \item theory can be retrieved from ctxt by Proof_Context.theory_of |
442 \item xxx |
440 \item xxx |
443 \item cleaup the many conversions string -- theory |
441 \item cleaup the many conversions string -- theory |
444 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ? |
442 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ? |
445 \item 1. Rewrite.eval_true_, then |
443 \item 1. Rewrite.eval_true_, then |
446 Lucin.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, Lucin.stac2tac. |
444 LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.stac2tac. |
447 \item fun associate |
445 \item fun associate |
448 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*) |
446 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*) |
449 \item xxx |
447 \item xxx |
450 \item xxx |
448 \item xxx |
451 \item xxx |
449 \item xxx |