1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Sun Apr 19 15:37:39 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Sun Apr 19 15:51:31 2020 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  *)
     1.5  theory BaseDefinitions imports Know_Store
     1.6  begin
     1.7 +  ML_file calcelems.sml
     1.8    ML_file termC.sml
     1.9    ML_file contextC.sml
    1.10    ML_file environment.sml

     2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 15:37:39 2020 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 15:51:31 2020 +0200
     2.3 @@ -35,7 +35,6 @@
     2.4  ML_file "celem-8.sml"  (*thydata*)
     2.5  ML_file "celem-91.sml" (*check_guhs_unique*)
     2.6  
     2.7 -ML_file calcelems.sml
     2.8  ML_file tracing.sml
     2.9  ML \<open>
    2.10  \<close> ML \<open>
    2.11 @@ -62,15 +61,15 @@
    2.12    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
    2.13    val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
    2.14    val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
    2.15 -  val get_cas: theory -> Celem.cas_elem list
    2.16 -  val add_cas: Celem.cas_elem list -> theory -> theory
    2.17 -  val get_ptyps: theory -> Celem.ptyps
    2.18 -  val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
    2.19 -  val get_mets: theory -> Celem.mets
    2.20 -  val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
    2.21 -  val get_thes: theory -> (Celem.thydata Celem1.ptyp) list
    2.22 -  val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    2.23 -  val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    2.24 +  val get_cas: theory -> Celem7.cas_elem list
    2.25 +  val add_cas: Celem7.cas_elem list -> theory -> theory
    2.26 +  val get_ptyps: theory -> Celem5.ptyps
    2.27 +  val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
    2.28 +  val get_mets: theory -> Celem6.mets
    2.29 +  val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
    2.30 +  val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list
    2.31 +  val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    2.32 +  val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    2.33    val get_ref_thy: unit -> theory
    2.34    val set_ref_thy: theory -> unit
    2.35  end;                               
    2.36 @@ -98,17 +97,17 @@
    2.37    fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
    2.38  
    2.39    structure Data = Theory_Data (
    2.40 -    type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
    2.41 +    type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list;
    2.42      val empty = [];
    2.43      val extend = I;
    2.44 -    val merge = merge Celem.cas_eq;
    2.45 +    val merge = merge Celem7.cas_eq;
    2.46      );                                                              
    2.47    fun get_cas thy = Data.get thy
    2.48 -  fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
    2.49 +  fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas)
    2.50  
    2.51    structure Data = Theory_Data (
    2.52 -    type T = Celem.ptyps;
    2.53 -    val empty = [Celem.e_Ptyp];
    2.54 +    type T = Celem5.ptyps;
    2.55 +    val empty = [Celem5.e_Ptyp];
    2.56      val extend = I;
    2.57      val merge = Celem1.merge_ptyps;
    2.58      );
    2.59 @@ -116,39 +115,39 @@
    2.60    fun add_pbts pbts thy = let
    2.61            fun add_pbt (pbt as {guh,...}, pblID) =
    2.62                  (* the pblID has the leaf-element as first; better readability achieved *)
    2.63 -                (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
    2.64 +                (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
    2.65                    rev pblID |> Celem1.insrt pblID pbt);
    2.66          in Data.map (fold add_pbt pbts) thy end;
    2.67  
    2.68    structure Data = Theory_Data (
    2.69 -    type T = Celem.mets;
    2.70 -    val empty = [Celem.e_Mets];
    2.71 +    type T = Celem6.mets;
    2.72 +    val empty = [Celem6.e_Mets];
    2.73      val extend = I;
    2.74      val merge = Celem1.merge_ptyps;
    2.75      );
    2.76    val get_mets = Data.get;
    2.77    fun add_mets mets thy = let
    2.78            fun add_met (met as {guh,...}, metID) =
    2.79 -                (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
    2.80 +                (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
    2.81                    Celem1.insrt metID met metID);
    2.82          in Data.map (fold add_met mets) thy end;
    2.83  
    2.84    structure Data = Theory_Data (
    2.85 -    type T = (Celem.thydata Celem1.ptyp) list;
    2.86 +    type T = (Celem8.thydata Celem1.ptyp) list;
    2.87      val empty = [];
    2.88      val extend = I;
    2.89      val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
    2.90      );                                                              
    2.91    fun get_thes thy = Data.get thy
    2.92    fun add_thes thes thy = let
    2.93 -    fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
    2.94 +    fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata
    2.95    in Data.map (fold add_the thes) thy end;
    2.96    fun insert_fillpats fis thy =
    2.97      let
    2.98        fun update_elem (theID, fillpats) =
    2.99          let
   2.100            val hthm = Celem1.get_py (Data.get thy) theID theID
   2.101 -          val hthm' = Celem.update_hthm hthm fillpats
   2.102 +          val hthm' = Celem8.update_hthm hthm fillpats
   2.103              handle ERROR _ =>
   2.104                error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
   2.105          in Celem1.update_ptyps theID theID hthm' end
   2.106 @@ -207,11 +206,11 @@
   2.107  section \<open>determine sequence of main parts in thehier\<close>
   2.108  setup \<open>
   2.109  KEStore_Elems.add_thes
   2.110 -  [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
   2.111 +  [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "",
   2.112      mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
   2.113 -  (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
   2.114 +  (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "",
   2.115      mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
   2.116 -  (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
   2.117 +  (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "",
   2.118      mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
   2.119  \<close>
   2.120  
   2.121 @@ -231,31 +230,31 @@
   2.122  fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
   2.123  
   2.124  (* we avoid term_to_string''' defined later *)
   2.125 -fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
   2.126 +fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
   2.127    "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
   2.128 -  (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
   2.129 +  (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
   2.130  
   2.131  fun count_kestore_ptyps [] = 0
   2.132    | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
   2.133        1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
   2.134  fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
   2.135        (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
   2.136 -val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
   2.137 +val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
   2.138  fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
   2.139 -fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
   2.140 +fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
   2.141  fun sort_kestore_ptyp' _ [] = []
   2.142    | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
   2.143       ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
   2.144         :: sort_kestore_ptyp' ordfun ps');
   2.145  val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
   2.146  
   2.147 -fun metguh2str ({guh,...} : Celem.met) = guh : string;
   2.148 -fun check_kestore_met (mp: Celem.met Celem1.ptyp) =
   2.149 +fun metguh2str ({guh,...} : Celem6.met) = guh : string;
   2.150 +fun check_kestore_met (mp: Celem6.met Celem1.ptyp) =
   2.151        check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
   2.152 -fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
   2.153 +fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
   2.154  val sort_kestore_met = sort_kestore_ptyp' met_ord;
   2.155  
   2.156 -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
   2.157 +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes
   2.158  fun write_thes thydata_list =
   2.159    thydata_list 
   2.160      |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))

     3.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Sun Apr 19 15:37:39 2020 +0200
     3.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Sun Apr 19 15:51:31 2020 +0200
     3.3 @@ -14,11 +14,7 @@
     3.4    ML_file interface.sml
     3.5  
     3.6  ML \<open>
     3.7 -open Celem6
     3.8  \<close> ML \<open>
     3.9 -val e_met = {guh = "met_empty", mathauthors = [], init = Celem3.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
    3.10 -	erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
    3.11 -	errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
    3.12  \<close> ML \<open>
    3.13  \<close>
    3.14  end
    3.15 \ No newline at end of file