equal
deleted
inserted
replaced
63 * WN: Step_Specify.initialisePIDE: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc |
63 * WN: Step_Specify.initialisePIDE: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc |
64 ? which uses initialisePIDE !? |
64 ? which uses initialisePIDE !? |
65 * WN: ? unify "no_met" with "empty_meth_id" from References.empty ? |
65 * WN: ? unify "no_met" with "empty_meth_id" from References.empty ? |
66 |
66 |
67 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle? |
67 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle? |
|
68 See notes in Build_Thydata.thy. |
68 https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes |
69 https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes |
69 several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and |
70 several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and |
70 "course designer (Kurs-Designer)". The latter just adds examples which re-use existing |
71 "course designer (Kurs-Designer)". The latter just adds examples which re-use existing |
71 knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter. |
72 knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter. |
72 KEStore_Elems.get_thes and KEStore_Elems.add_thes are ONLY required for the Lucas-Interpreter |
73 KEStore_Elems.get_thes and KEStore_Elems.add_thes are ONLY required for the Lucas-Interpreter |