1.1 --- a/TODO.md Sat Aug 14 18:49:36 2021 +0200
1.2 +++ b/TODO.md Sat Aug 14 18:59:30 2021 +0200
1.3 @@ -20,6 +20,9 @@
1.4
1.5 * KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge?
1.6 (Exception: rlss with its special cross-theory merge.)
1.7 + ? how adapt the different signatures ?
1.8 + union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
1.9 + merge : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
1.10
1.11 * What is the purpose of "#numeral" instead of plain numeral?
1.12 ??
1.13 @@ -41,7 +44,7 @@
1.14 * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
1.15 e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
1.16
1.17 -* WN: Avoid Thm.get_name_hintand use Global_Theory.get_thm instead, get theory from References.T
1.18 +* WN: Avoid Thm.get_name_hint and use Global_Theory.get_thm instead, get theory from References.T
1.19 and push theory through as argument of respective functions.
1.20
1.21 * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations