1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Jul 31 16:35:33 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 03 13:22:36 2022 +0200
     1.3 @@ -43,6 +43,8 @@
     1.4  ML_file "problem-def.sml"
     1.5  ML_file "method-def.sml"
     1.6  ML_file "cas-def.sml"
     1.7 +ML_file "formalise.sml"
     1.8 +ML_file "example.sml"
     1.9  ML_file "thy-write.sml"
    1.10  
    1.11  ML \<open>
    1.12 @@ -76,6 +78,8 @@
    1.13    val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
    1.14    val get_mets: theory -> Meth_Def.store
    1.15    val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
    1.16 +  val get_expls: theory -> Example.store
    1.17 +  val add_expls: (Example.T * Store.key) list -> theory -> theory
    1.18    val get_thes: theory -> (Thy_Write.thydata Store.node) list
    1.19    val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.20    val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory 
    1.21 @@ -144,6 +148,18 @@
    1.22      in Data.map (fold add_met mets) thy end;
    1.23  
    1.24    structure Data = Theory_Data (
    1.25 +    type T = Example.store;
    1.26 +    val empty = [Example.empty_store];
    1.27 +    val extend = I;
    1.28 +    val merge = Store.merge;
    1.29 +    );
    1.30 +  val get_expls = Data.get;
    1.31 +  fun add_expls expls thy =
    1.32 +    let
    1.33 +      fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
    1.34 +    in Data.map (fold add_expl expls) thy end;
    1.35 +
    1.36 +  structure Data = Theory_Data (
    1.37      type T = (Thy_Write.thydata Store.node) list;
    1.38      val empty = [];
    1.39      val extend = I;
    1.40 @@ -257,6 +273,7 @@
    1.41  fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
    1.42  fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
    1.43  fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
    1.44 +fun get_expls () = get_ref_thy () |> KEStore_Elems.get_expls;
    1.45  \<close>
    1.46  
    1.47  rule_set_knowledge