1.1 --- a/src/Tools/isac/TODO.thy	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -26,12 +26,6 @@
     1.4  (*/------- to  -------\*)
     1.5  (*\------- to  -------/*)
     1.6    \begin{itemize}
     1.7 -  \item type_empty -> typ_empty
     1.8 -  \item Seqence -> Sequence
     1.9 -  \item EmptyScr -> Empty_Prog
    1.10 -  \item Num_Calc -> Exec, eval_* -> exec_*
    1.11 -  \item xxx
    1.12 -  \item xxx
    1.13    \item ML_file "rule-set.sml" KEStore -> MathEngBasic (=ThmC, Rewrite)
    1.14      probably first review calcelems.sml
    1.15    \item xxx
    1.16 @@ -227,7 +221,7 @@
    1.17       (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
    1.18       (*+*)  prls =
    1.19       (*+*)    Rls {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =
    1.20 -     (*+*)      ("dummy_ord", fn), rules = [], scr = EmptyScr, srls = Erls}:
    1.21 +     (*+*)      ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Erls}:
    1.22       (*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
    1.23       (*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
    1.24       (*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x' *)
    1.25 @@ -424,7 +418,7 @@
    1.26  \<close>
    1.27  subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
    1.28  text \<open>
    1.29 -remove refactor Rfuns, Rule.Prog, Rule.EmptyScr, RrlsState: this is a concept never brought to work.
    1.30 +remove refactor Rfuns, Rule.Prog, Rule.Empty_Prog, RrlsState: this is a concept never brought to work.
    1.31    Clarify relation to reverse rewriting!
    1.32    \begin{itemize}
    1.33    \item separate mut.recursion program with rule and rls by deleting fild scr in rls