1.1 --- a/TODO.md Wed May 26 13:42:53 2021 +0200
1.2 +++ b/TODO.md Wed May 26 14:10:17 2021 +0200
1.3 @@ -31,6 +31,16 @@
1.4 * Check/clarify Context.theory_name vs. Context.theory_long_name.
1.5
1.6
1.7 +* WN: remove always empty arguments in MethodC.prep_input and Problem.prep_input
1.8 + (following the "TODO" comment);
1.9 +
1.10 +* WN: eliminate ThyC.to_ctxt, use Proof_Context.init_global inline to make more
1.11 + clear where the normal Isabelle context-discipline is bypassed;
1.12 +
1.13 +* WN: standardize theory for KEStore_Elems.add_rlss, KEStore_Elems.add_mets, KEStore_Elems.add_pbts
1.14 + - should be always the current @{theory} of the enclosing "setup" command;
1.15 + - avoid old-style "val thy = @{theory}" somewhere in a theory file;
1.16 +
1.17 * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
1.18 - quite often "axiomatization ..." can be turned into "lemma ... by auto"
1.19 without further ado;