diff -r cc5b51681c4b -r 87336f3b021f src/Tools/isac/TODO.thy --- a/src/Tools/isac/TODO.thy Sat May 02 17:39:04 2020 +0200 +++ b/src/Tools/isac/TODO.thy Mon May 04 09:25:51 2020 +0200 @@ -115,14 +115,8 @@ use this also for me, not only for me_ist_ctxt; del. me this requires much updating in all test/* \item xxx - \item xxx - \item generate, generate1: NO thy as arg. - Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec - redesign return value (originally for output by fun me?) - \item xxx \item shift tests into NEW model.sml (upd, upds_envv, ..) \item xxx - \item xxx \item clarify handling of contexts ctxt ContextC \begin{itemize} \item xxx @@ -298,7 +292,6 @@ \begin{itemize} \item *.check | *.add Specify_Step.add <-- Generate.generate1 - Solve_Step.add <-- Generate.generate1 \item xxx \end{itemize} \item xxx