1.1 --- a/TODO.md	Sat Aug 14 20:38:23 2021 +0200
     1.2 +++ b/TODO.md	Sat Aug 14 21:40:55 2021 +0200
     1.3 @@ -10,6 +10,11 @@
     1.4      76a77
     1.5      >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
     1.6  
     1.7 +* MW: exception TYPE raised by Skip_Proof.make_thm, see
     1.8 +    https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
     1.9 +
    1.10 +* MW: error with \<^rule_thm>\<open>filterVar.simps(1)\<close>
    1.11 +    https://hg.risc.uni-linz.ac.at/wneuper/isa/diff/4f5f29fd0af9/src/Tools/isac/Knowledge/DiffApp.thy#l1.34
    1.12  
    1.13  * Eliminate Thy_Info.get_theory eventually: should take theory from ancestory
    1.14    within current context.
    1.15 @@ -54,8 +59,7 @@
    1.16      - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
    1.17      - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
    1.18  
    1.19 -* WN: eliminate ThmC.numerals_to_Free, done except 1 error:
    1.20 -  + exception TYPE raised by Skip_Proof.make_thm, several inherited errors in tests marked TOODOO.1
    1.21 +* WN: eliminate ThmC.numerals_to_Free, check tests marked TOODOO.1
    1.22    + ? how do algebraic operations on numerals ? Presburger ? simplifier ? hack see
    1.23      https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
    1.24