1.1 --- a/TODO.md	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/TODO.md	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -69,6 +69,9 @@
     1.4  
     1.5  * WN: improve naming in refine.sml, m-match.sml
     1.6  * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›
     1.7 +* WN: review Prog_Tac:
     1.8 +      (*+isa==isa2*)@{term "Substitution []"};               (*Free ("Subproblem",.. ALSO Subproblem, ?!*)
     1.9 +      (*+isa==isa2*)@{term "Rewrite_Set ''norm_Rational''"}; (*Const ("Prog_Tac.Rewrite_Set",..*)
    1.10  * WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes:
    1.11      (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys
    1.12      (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them.