1.1 --- a/src/Tools/isac/TODO.thy	Tue May 05 15:39:20 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Thu May 07 11:04:02 2020 +0200
     1.3 @@ -27,6 +27,8 @@
     1.4  (*\------- to  from -------/*)
     1.5    \begin{itemize}
     1.6    \item xxx
     1.7 +  \item fun specify_init_calc defined twice
     1.8 +  \item xxx
     1.9    \item push nes identifiers back from O/I_Model to Model_Def
    1.10    \item xxx
    1.11    \item rename Tactic.Calculate -> Tactic.Evaluate
    1.12 @@ -55,6 +57,8 @@
    1.13  text \<open>
    1.14    \begin{itemize}
    1.15    \item xxx
    1.16 +  \item ctxt is superfluous in specify-phase due to type constraints from Descript.thy
    1.17 +  \item xxx
    1.18    \item Derive.do_one: TODO find code in common with complete_solve
    1.19          Derive.embed: TODO rewrite according to CAO (+ no intermediate access to Ctree)
    1.20    \item xxx