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