scalable version of Named_Thms, using Item_Net;
authorwenzelm
Thu Nov 05 20:40:16 2009 +0100 (2009-11-05)
changeset 33453fe551dc9d4bd
parent 33452 c7175a18c090
child 33454 485fd398dd33
scalable version of Named_Thms, using Item_Net;
src/Pure/Tools/named_thms.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/Tools/named_thms.ML	Thu Nov 05 17:59:49 2009 +0100
     1.2 +++ b/src/Pure/Tools/named_thms.ML	Thu Nov 05 20:40:16 2009 +0100
     1.3 @@ -1,8 +1,7 @@
     1.4  (*  Title:      Pure/Tools/named_thms.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Named collections of theorems in canonical order.  Based on naive data
     1.8 -structures -- not scalable!
     1.9 +Named collections of theorems in canonical order.
    1.10  *)
    1.11  
    1.12  signature NAMED_THMS =
    1.13 @@ -20,22 +19,23 @@
    1.14  
    1.15  structure Data = GenericDataFun
    1.16  (
    1.17 -  type T = thm list;
    1.18 -  val empty = [];
    1.19 +  type T = thm Item_Net.T;
    1.20 +  val empty = Thm.full_rules;
    1.21    val extend = I;
    1.22 -  fun merge _ = Thm.merge_thms;
    1.23 +  fun merge _ = Item_Net.merge;
    1.24  );
    1.25  
    1.26 -val get = Data.get o Context.Proof;
    1.27 +val content = Item_Net.content o Data.get;
    1.28 +val get = content o Context.Proof;
    1.29  
    1.30 -val add_thm = Data.map o Thm.add_thm;
    1.31 -val del_thm = Data.map o Thm.del_thm;
    1.32 +val add_thm = Data.map o Item_Net.update;
    1.33 +val del_thm = Data.map o Item_Net.remove;
    1.34  
    1.35  val add = Thm.declaration_attribute add_thm;
    1.36  val del = Thm.declaration_attribute del_thm;
    1.37  
    1.38  val setup =
    1.39    Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
    1.40 -  PureThy.add_thms_dynamic (Binding.name name, Data.get);
    1.41 +  PureThy.add_thms_dynamic (Binding.name name, content);
    1.42  
    1.43  end;
     2.1 --- a/src/Pure/more_thm.ML	Thu Nov 05 17:59:49 2009 +0100
     2.2 +++ b/src/Pure/more_thm.ML	Thu Nov 05 20:40:16 2009 +0100
     2.3 @@ -48,6 +48,7 @@
     2.4    val add_thm: thm -> thm list -> thm list
     2.5    val del_thm: thm -> thm list -> thm list
     2.6    val merge_thms: thm list * thm list -> thm list
     2.7 +  val full_rules: thm Item_Net.T
     2.8    val intro_rules: thm Item_Net.T
     2.9    val elim_rules: thm Item_Net.T
    2.10    val elim_implies: thm -> thm -> thm
    2.11 @@ -246,6 +247,7 @@
    2.12  val del_thm = remove eq_thm_prop;
    2.13  val merge_thms = merge eq_thm_prop;
    2.14  
    2.15 +val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
    2.16  val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of);
    2.17  val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);
    2.18