1.1 --- a/TODO.md	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/TODO.md	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -85,6 +85,16 @@
     1.4    val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
     1.5  \<close>
     1.6  
     1.7 +* WN: rewriting with ctxt not complete (cause errors hard to indentify later)
     1.8 +    - Prconditions.eval
     1.9 +    - Solve_Step.check ..Rewrite_Inst, Substitute, ..
    1.10 +    - Error_Pattern.check_for', fill_form
    1.11 +    - Derive.steps
    1.12 +    - Fetch_Tacs.specific_from_prog ?
    1.13 +    - ? LIST IS NOT COMPLETE
    1.14 +
    1.15 +* WN: ? Rational.Cancel_p; extend use of \<^theory> to \<^theory_context>
    1.16 +
    1.17  * WN: redesign transition from Specification to Solution: how relate 
    1.18      - Formalise.model with variants (e.g. VSCode_Example)
    1.19        reconsider separation of variants F_I, F_II, see MAWEN paper