1.1 --- a/src/Tools/isac/TODO.thy	Thu Mar 26 16:17:21 2020 +0100
     1.2 +++ b/src/Tools/isac/TODO.thy	Tue Mar 31 13:06:41 2020 +0200
     1.3 @@ -25,6 +25,20 @@
     1.4  text \<open>
     1.5    \begin{itemize}
     1.6    \item xxx
     1.7 +  \item xxx
     1.8 +  \item LI.do_next (*TODO RM..*)
     1.9 +  \item xxx
    1.10 +  \item  RENAME ARGS ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
    1.11 +  \item xxx
    1.12 +  \item RM asm FROM Check_Postcond' (pI, (prog_res, asm)) ... asms are handled by ctxt !
    1.13 +  \item xxx
    1.14 +  \item generate.sml: RM datatype edit = EdUndef | Write | Protect
    1.15 +  \item xxx
    1.16 +  \item ad ERROR @unknown fact all_left in Test_Isac: search "Undefined"
    1.17 +    Undef -> Real_Undef
    1.18 +  \item xxx
    1.19 +  \item TermC.list2isalist: typ -> term list -> term  .. should NOT requires typ
    1.20 +  \item xxx
    1.21    \item restore clarity of  "trace_rewrite": "=====" seems to be lost:
    1.22      #####  try calc: HOL.eq'    <<<------------------------------- here the error comes from
    1.23      =====  calc. to: ~ False    <<<------------------------------- \<not> x = 0 is NOT False
    1.24 @@ -62,7 +76,7 @@
    1.25    \item renamings
    1.26      \begin{itemize}
    1.27      \item NotAss -> Not_Associated | Ass -> Associated
    1.28 -    \item ContextC.from_subpbl_to_caller -> subpbl_to_caller
    1.29 +    \item ContextC.subpbl_to_caller -> subpbl_to_caller
    1.30      \item Tactic.is_empty_tac -> Tactic.is_empty
    1.31      \item Istate.istate2str -> Istate.string_of
    1.32      \item xxx
    1.33 @@ -641,6 +655,15 @@
    1.34  \begin{itemize}
    1.35  \item xxx
    1.36  \item xxx
    1.37 +\item ?OK Test_Isac_Short with
    1.38 +    LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
    1.39 +  instead
    1.40 +    LI.by_tactic tac (Istate.e_istate, ContextC.e_ctxt) ptp
    1.41 +  in step-solve ?
    1.42 +\item xxx
    1.43 +\item test from last CS with outcommented re-def of code -> 
    1.44 +  -> \<open>further tests additional to src/.. files\<close>
    1.45 +      ADDTESTS/redefined-code.sml
    1.46  \item xxx
    1.47  \item efb749b79361 Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:
    1.48    ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"