1.1 --- a/src/Tools/isac/TODO.thy	Sat May 02 17:39:04 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Mon May 04 09:25:51 2020 +0200
     1.3 @@ -115,14 +115,8 @@
     1.4        use this also for me, not only for me_ist_ctxt; del. me
     1.5        this requires much updating in all test/*
     1.6    \item xxx
     1.7 -  \item xxx
     1.8 -  \item generate, generate1: NO thy as arg.
     1.9 -        Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
    1.10 -        redesign return value (originally for output by fun me?)
    1.11 -  \item xxx
    1.12    \item shift tests into NEW model.sml (upd, upds_envv, ..)
    1.13    \item xxx
    1.14 -  \item xxx
    1.15    \item clarify handling of contexts ctxt ContextC
    1.16      \begin{itemize}
    1.17      \item xxx
    1.18 @@ -298,7 +292,6 @@
    1.19        \begin{itemize}
    1.20        \item *.check | *.add
    1.21          Specify_Step.add <-- Generate.generate1
    1.22 -        Solve_Step.add   <-- Generate.generate1
    1.23        \item xxx
    1.24        \end{itemize}
    1.25      \item xxx