1.1 --- a/TODO.md	Tue Aug 17 21:57:40 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 17 22:39:48 2021 +0200
     1.3 @@ -10,12 +10,6 @@
     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      cf. e587c45cae0f note in Build_Thydata.thy