1.1 --- a/src/Tools/isac/TODO.thy Mon Jun 29 17:33:47 2020 +0200
1.2 +++ b/src/Tools/isac/TODO.thy Mon Jun 29 18:05:04 2020 +0200
1.3 @@ -63,6 +63,15 @@
1.4 text \<open>
1.5 \begin{itemize}
1.6 \item xxx
1.7 + \item make steps around SubProblem more consistent:
1.8 + SubProblem (thy, [pbl]) is bypassed by Model_Problem, if it is 1st Tactic in a Program.
1.9 + Design:
1.10 + * the Tactic SubProblem (thy, [pbl]) creates the formula SubProblem (thy, [pbl])
1.11 + (only the headline !)
1.12 + * the Tactic Model_Problem starts Specification
1.13 + (with an empty Model)
1.14 + see test/../sub-problem.sml
1.15 + \item xxx
1.16 \item Specify_Step.add has dummy argument Istate_Def.Uistate -- remove down to Ctree
1.17 \item xxx
1.18 \item Step_Specify.by_tactic (Tactic.Model_Problem' (id, _, met))