1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Aug 03 18:06:02 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Aug 03 18:17:27 2022 +0200
1.3 @@ -87,7 +87,7 @@
1.4 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.5 val get_ref_thy: unit -> theory
1.6 val set_ref_thy: theory -> unit
1.7 -end;
1.8 +end;
1.9
1.10 structure KEStore_Elems(**): KESTORE_ELEMS(**) =
1.11 struct
1.12 @@ -247,8 +247,9 @@
1.13
1.14 section \<open>Re-use existing access functions for knowledge elements\<close>
1.15 text \<open>
1.16 - The independence of problems' and methods' structure enforces the accesse
1.17 - functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
1.18 + The independence of problems' and methods' structure from theory dependency structure
1.19 + enforces the access functions to use "Isac_Knowledge",
1.20 + the final theory which comprises all knowledge defined.
1.21 \<close>
1.22 ML \<open>
1.23 val get_ref_thy = KEStore_Elems.get_ref_thy;