1.1 --- a/src/Tools/isac/TODO.thy	Mon May 04 09:25:51 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Mon May 04 10:19:16 2020 +0200
     1.3 @@ -23,8 +23,8 @@
     1.4  \<close>
     1.5  subsection \<open>Current changeset\<close>
     1.6  text \<open>
     1.7 -(*/------- to  -------\*)
     1.8 -(*\------- to  -------/*)
     1.9 +(*/------- to  from  -------\*)
    1.10 +(*\------- to  from  -------/*)
    1.11    \begin{itemize}
    1.12    \item xxx
    1.13    \item rm warnings from solve-step.sml
    1.14 @@ -288,12 +288,7 @@
    1.15    \item xxx
    1.16    \item re-organise code for Interpret
    1.17      \begin{itemize}
    1.18 -    \item Step*: Step_Specify | Step_Solve | Step
    1.19 -      \begin{itemize}
    1.20 -      \item *.check | *.add
    1.21 -        Specify_Step.add <-- Generate.generate1
    1.22 -      \item xxx
    1.23 -      \end{itemize}
    1.24 +    \item Step*: Step_Specify | Step_Solve | Step DONE
    1.25      \item xxx
    1.26      \item Prog_Tac: fun get_first_argument takes both Prog_Tac + Program --- wait for separate Tactical
    1.27        then shift into common descendant
    1.28 @@ -408,7 +403,7 @@
    1.29    \item cleaup the many conversions string -- theory
    1.30    \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
    1.31    \item 1. Rewrite.eval_true_, then
    1.32 -    LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.tac_from_prog.
    1.33 +    LItool.check_leaf, Rewrite.eval_prog_expr, Step.add, LItool.tac_from_prog.
    1.34    \item fun associate
    1.35      let val thy = ThyC.get_theory "Isac_Knowledge";(*TODO*)
    1.36    \item xxx