1.1 --- a/src/Tools/isac/TODO.thy Thu Dec 19 16:41:57 2019 +0100
1.2 +++ b/src/Tools/isac/TODO.thy Thu Dec 19 16:53:52 2019 +0100
1.3 @@ -84,20 +84,20 @@
1.4 \begin{itemize}
1.5 \item Step_Specify.check <-- Applicable.applicable_in
1.6 \item Step_Specify.add <-- Generate.generate1
1.7 - \item Step_Specify.by_tactic : Tactic.input -> Ctree.state -> step_result
1.8 - \item Step_Specify.by_formula: ?term? -> Ctree.state -> step_result
1.9 - \item Step_Specify.find_next : Ctree.state -> step_result
1.10 + \item Step_Specify.by_tactic : Tactic.input -> Ctree.state -> ...stay as is
1.11 + \item Step_Specify.by_formula: ?term? -> Ctree.state -> .............
1.12 + \item Step_Specify.find_next : Ctree.state -> ...
1.13 \end{itemize}
1.14 \item Step_Solve in Interpret/step-solve.sml
1.15 \begin{itemize}
1.16 \item Step_Solve.check <-- Applicable.applicable_in
1.17 inserts all data into Tactic.T available -- not all are at time of call!
1.18 \item Step_Solve.add <-- Generate.generate1
1.19 - \item Step_Solve.by_tactic : Tactic.input -> Ctree.state -> step_result
1.20 - ^^^^LucinNEW,begin_end_prog
1.21 - \item Step_Solve.by_formula : term -> Ctree.state -> step_result
1.22 - \item Step_Solve.find_next : Ctree.state -> step_result
1.23 - ^^^^LucinNEW,do_solve_step; Apply_Method ever used???
1.24 + \item Step_Solve.by_tactic : Tactic.input -> Ctree.state -> ...
1.25 + ^^^^LucinNEW.begin_end_prog
1.26 + \item Step_Solve.by_formula : term -> Ctree.state -> ...
1.27 + \item Step_Solve.find_next : Ctree.state -> ...
1.28 + ^^^^LucinNEW.do_solve_step
1.29 \end{itemize}
1.30 \item Step in MathEngine/step.sml
1.31 \begin{itemize}
1.32 @@ -114,7 +114,7 @@
1.33 \begin{itemize}
1.34 \item rename Calc --> Calc_
1.35 \item ? type Calc.T = CTree.state ?
1.36 - \item Calc.add_step <-- Step_Specify.add + Step_Solve.add <-- Generate.generate*
1.37 + \item Calc.add_step <-- ???_Specify.add + ???_Solve.add <-- Generate.generate*
1.38 \item xxx
1.39 \end{itemize}
1.40 \item xxx