1.1 --- a/TODO.md	Sat Aug 06 18:00:33 2022 +0200
     1.2 +++ b/TODO.md	Sat Aug 06 18:50:43 2022 +0200
     1.3 @@ -55,7 +55,6 @@
     1.4  ***** priority of WN items is top down, most urgent/simple on top
     1.5  
     1.6  * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
     1.7 -    - Derive.steps
     1.8      - Fetch_Tacs.specific_from_prog ?
     1.9      - Eval.adhoc_thm, adhoc_thm1_
    1.10      - ? LIST IS NOT COMPLETE
    1.11 @@ -67,6 +66,7 @@
    1.12          val thy = ThyC.get_theory thy';              ->   val thy = Proof_Context.theory_of ctxt
    1.13          val ctxt = Proof_Context.init_global thy;    ->   val thy' = Context.theory_name thy
    1.14        cp code to test/*
    1.15 +    - Derive.steps: note HACK
    1.16  
    1.17  * WN: eliminate SPARK; as an example replaced by Outer_Syntax.command..problem
    1.18