src/Tools/isac/BaseDefinitions/Know_Store.thy
changeset 60508 ce09935439b3
parent 60506 145e45cd7a0f
child 60509 2e0b7ca391dc
     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;