1.1 --- a/TODO.md	Sun Jul 31 13:45:20 2022 +0200
     1.2 +++ b/TODO.md	Sun Jul 31 16:35:33 2022 +0200
     1.3 @@ -85,12 +85,15 @@
     1.4    val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
     1.5  \<close>
     1.6  
     1.7 +* WN: Calculate.the: add structure Calculate
     1.8 +
     1.9  * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
    1.10      - Prconditions.eval
    1.11      - Solve_Step.check ..Rewrite_Inst, Substitute, ..
    1.12      - Error_Pattern.check_for', fill_form
    1.13      - Derive.steps
    1.14      - Fetch_Tacs.specific_from_prog ?
    1.15 +    - Eval.adhoc_thm, adhoc_thm1_
    1.16      - ? LIST IS NOT COMPLETE
    1.17  
    1.18  * WN: ? Rational.Cancel_p; extend use of \<^theory> to \<^theory_context>