1.1 --- a/src/Tools/isac/TODO.thy	Tue Dec 08 17:10:18 2020 +0100
     1.2 +++ b/src/Tools/isac/TODO.thy	Wed Dec 09 14:22:24 2020 +0100
     1.3 @@ -28,6 +28,11 @@
     1.4    \begin{itemize}
     1.5    \item xxx
     1.6    \item xxx
     1.7 +  \item Input_Descript.descriptor -> Input_Descript.T
     1.8 +  \item xxx
     1.9 +  \item Step_Specify.initialisePIDE: remove hdl in return-value
    1.10 +        rename Step_Specify.nxt_specify_init_calc
    1.11 +  \item xxx
    1.12    \item relate Prog_Epxr.lhs to Thm.lhs_of
    1.13    \item xxx
    1.14    \item as soon as src/../parseC.sml is stable,
    1.15 @@ -91,7 +96,7 @@
    1.16    \item xxx
    1.17    \item revise O_Model and I_Model with an example with more than 1 variant.
    1.18    \item xxx
    1.19 -  \item ctxt is superfluous in specify-phase due to type constraints from Descript.thy
    1.20 +  \item ctxt is superfluous in specify-phase due to type constraints from Input_Descript.thy
    1.21    \item xxx
    1.22    \item Derive.do_one: TODO find code in common with complete_solve
    1.23          Derive.embed: TODO rewrite according to CAO (+ no intermediate access to Ctree)