equal
deleted
inserted
replaced
19 |
19 |
20 * KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge? |
20 * KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge? |
21 (Exception: rlss with its special cross-theory merge.) |
21 (Exception: rlss with its special cross-theory merge.) |
22 |
22 |
23 * What is the purpose of "#numeral" instead of plain numeral? |
23 * What is the purpose of "#numeral" instead of plain numeral? |
|
24 ?? |
24 |
25 |
25 * Check/clarify Context.theory_name vs. Context.theory_long_name. |
26 * Check/clarify Context.theory_name vs. Context.theory_long_name. |
26 |
27 |
27 * Eliminate mutable Rewrite_Ord.rew_ord' (!?); |
28 * Eliminate mutable Rewrite_Ord.rew_ord' (!?); |
28 shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy |
29 shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy |
30 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle? |
31 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle? |
31 https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes |
32 https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes |
32 several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and |
33 several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and |
33 "course designer (Kurs-Designer)". The latter just adds examples which re-use existing |
34 "course designer (Kurs-Designer)". The latter just adds examples which re-use existing |
34 knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter. |
35 knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter. |
35 |
|
36 * WN: clarify add_calcs with non-existant constant "Integrate.add_new_c"; |
|
37 |
36 |
38 * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations, |
37 * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations, |
39 e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try"; |
38 e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try"; |
40 |
39 |
41 * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by |
40 * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by |