src/Tools/isac/TODO.thy
changeset 60026 edd86bf5113b
parent 60017 cdcc5eba067b
child 60040 a05df90c0dee
     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))