1.1 --- a/TODO.md	Sun Jun 19 16:55:13 2022 +0200
     1.2 +++ b/TODO.md	Mon Jun 20 09:56:48 2022 +0200
     1.3 @@ -66,8 +66,9 @@
     1.4    val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
     1.5  \<close>
     1.6  
     1.7 -* WN: for calculation by use of Makarius' "problem" as boilerplate clarify:
     1.8 -    - How inspect Token lists, e.g. from ML_Lex.read OR ML_Lex.read_source ?
     1.9 -    - Why the ERROR in Demo_Example.thy at: \<open>problem pbl_bieg : "Biegelinien" = ..\<close> ?
    1.10 -    - 
    1.11 +* WN: redesign transition from Specification to Solution: how relate 
    1.12 +    - Formalise.model with variants (e.g. VSCode_Example)
    1.13 +      reconsider separation of variants F_I, F_II, see MAWEN paper
    1.14 +    - !?! I_Model of MethodC          (fairly free sequence, dependent on Formalise.model)
    1.15 +    - !?! formal arguments of program (fixed sequence)
    1.16