1.1 --- a/src/Tools/isac/TODO.thy	Tue Apr 14 15:56:15 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Wed Apr 15 10:07:43 2020 +0200
     1.3 @@ -23,6 +23,8 @@
     1.4  \<close>
     1.5  subsection \<open>Current changeset\<close>
     1.6  text \<open>
     1.7 +(*/------- to  -------\*)
     1.8 +(*\------- to  -------/*)
     1.9    \begin{itemize}
    1.10    \item type_empty -> typ_empty
    1.11    \item Seqence -> Sequence
    1.12 @@ -30,7 +32,8 @@
    1.13    \item Num_Calc -> Exec, eval_* -> exec_*
    1.14    \item xxx
    1.15    \item xxx
    1.16 -  \item xxx
    1.17 +  \item ML_file "rule-set.sml" KEStore -> MathEngBasic (=ThmC, Rewrite)
    1.18 +    probably first review calcelems.sml
    1.19    \item xxx
    1.20    \item xxx
    1.21    \item xxx
    1.22 @@ -50,7 +53,7 @@
    1.23      thmDeriv         : type for thy_hierarchy ONLY
    1.24      obsolete types   : thm' (SEE "ad thm'"), thm''. 
    1.25      revise funs      : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
    1.26 -    activate         : thmID_of_derivation_name'
    1.27 +    activate         : ThmC.cut_id'
    1.28      *)
    1.29    \item xxx
    1.30    \item use "Exec_Def" for renaming identifiers