--- a/src/Pure/more_thm.ML Tue Mar 17 14:12:06 2009 +0100
+++ b/src/Pure/more_thm.ML Tue Mar 17 14:12:43 2009 +0100
@@ -33,6 +33,8 @@
val add_thm: thm -> thm list -> thm list
val del_thm: thm -> thm list -> thm list
val merge_thms: thm list * thm list -> thm list
+ val intro_rules: thm Item_Net.T
+ val elim_rules: thm Item_Net.T
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
@@ -213,6 +215,12 @@
val merge_thms = merge eq_thm_prop;
+(* indexed collections *)
+
+val intro_rules = Item_Net.init eq_thm_prop Thm.concl_of;
+val elim_rules = Item_Net.init eq_thm_prop Thm.major_prem_of;
+
+
(** basic derived rules **)