equal
deleted
inserted
replaced
85 val get_thes: theory -> (Thy_Write.thydata Store.node) list |
85 val get_thes: theory -> (Thy_Write.thydata Store.node) list |
86 val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
86 val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
87 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory |
87 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory |
88 val get_ref_thy: unit -> theory |
88 val get_ref_thy: unit -> theory |
89 val set_ref_thy: theory -> unit |
89 val set_ref_thy: theory -> unit |
90 end; |
90 end; |
91 |
91 |
92 structure KEStore_Elems(**): KESTORE_ELEMS(**) = |
92 structure KEStore_Elems(**): KESTORE_ELEMS(**) = |
93 struct |
93 struct |
94 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
94 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
95 |
95 |
245 \<close> |
245 \<close> |
246 |
246 |
247 |
247 |
248 section \<open>Re-use existing access functions for knowledge elements\<close> |
248 section \<open>Re-use existing access functions for knowledge elements\<close> |
249 text \<open> |
249 text \<open> |
250 The independence of problems' and methods' structure enforces the accesse |
250 The independence of problems' and methods' structure from theory dependency structure |
251 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined. |
251 enforces the access functions to use "Isac_Knowledge", |
|
252 the final theory which comprises all knowledge defined. |
252 \<close> |
253 \<close> |
253 ML \<open> |
254 ML \<open> |
254 val get_ref_thy = KEStore_Elems.get_ref_thy; |
255 val get_ref_thy = KEStore_Elems.get_ref_thy; |
255 |
256 |
256 fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2") |
257 fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2") |