60 subsubsection ‹Start Example with a CAS_Cmd› |
60 subsubsection ‹Start Example with a CAS_Cmd› |
61 |
61 |
62 |
62 |
63 ***** priority of WN items is top down, most urgent/simple on top |
63 ***** priority of WN items is top down, most urgent/simple on top |
64 |
64 |
65 * WN: follow up 5b: clarify TermC.parse_patt/*_PIDE analogous to TermC.parse_strict/*_PIDE |
65 * WN: follow up 5d: clarify TermC.parse_patt/*_PIDE analogous to TermC.parse_strict/*_PIDE |
66 follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context} |
66 follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context} |
67 Thus eliminate use of Thy_Info.get_theory |
67 Thus eliminate use of Thy_Info.get_theory |
68 follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__" |
68 follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__" |
69 |
69 |
70 * WN: improve naming in refine.sml, m-match.sml |
70 * WN: improve naming in refine.sml, m-match.sml |
71 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store› |
71 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store› |
72 * WN: eliminate KEStore_Elems.get_thes, add_thes |
72 * WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes: |
73 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle? |
73 (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys |
74 See notes in Build_Thydata.thy. |
74 (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them. |
75 https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes |
75 adapt KEStore_Elems.insert_fillpats for that purpose. |
76 several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and |
|
77 "course designer (Kurs-Designer)". The latter just adds examples which re-use existing |
|
78 knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter. |
|
79 KEStore_Elems.get_thes and KEStore_Elems.add_thes are ONLY required for the Lucas-Interpreter |
|
80 retrieving Thm and Rls from string-identifiers (which do NOT indicate the theory of) -- |
|
81 -- get_thes and add_thes are the main reason for (b) |
|
82 So: How can KEStore_Elems.get_thes and KEStore_Elems.add_thes be replaced in current Isabelle? |
|
83 |
76 |
84 * WN: Specify/formalise.sml is in BaseDefinitions/ AND Specify/ DELETE ONE VERSION |
77 * WN: Specify/formalise.sml is in BaseDefinitions/ AND Specify/ DELETE ONE VERSION |
85 * WN: Step_Specify.initialise: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc |
78 * WN: Step_Specify.initialise: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc |
86 ? which uses initialise !? |
79 ? which uses initialise !? |
87 * WN: ? unify "no_met" with "empty_meth_id" from References.empty ? |
80 * WN: ? unify "no_met" with "empty_meth_id" from References.empty ? |