removed add/del_rules;
authorwenzelm
Fri Feb 03 23:12:30 2006 +0100 (2006-02-03 ago)
changeset 18922b05a2952de73
parent 18921 f47c46d7d654
child 18923 34f9df073ad9
removed add/del_rules;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri Feb 03 23:12:28 2006 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Feb 03 23:12:30 2006 +0100
     1.3 @@ -99,8 +99,6 @@
     1.4    val compose_single: thm * int * thm -> thm
     1.5    val add_rule: thm -> thm list -> thm list
     1.6    val del_rule: thm -> thm list -> thm list
     1.7 -  val add_rules: thm list -> thm list -> thm list
     1.8 -  val del_rules: thm list -> thm list -> thm list
     1.9    val merge_rules: thm list * thm list -> thm list
    1.10    val imp_cong_rule: thm -> thm -> thm
    1.11    val beta_eta_conversion: cterm -> thm
    1.12 @@ -588,11 +586,9 @@
    1.13  val size_of_thm = size_of_term o Thm.full_prop_of;
    1.14  
    1.15  (*maintain lists of theorems --- preserving canonical order*)
    1.16 -fun del_rules rs rules = Library.gen_rems eq_thm_prop (rules, rs);
    1.17 -fun add_rules rs rules = rs @ del_rules rs rules;
    1.18 -val del_rule = del_rules o single;
    1.19 -val add_rule = add_rules o single;
    1.20 -fun merge_rules (rules1, rules2) = gen_merge_lists' eq_thm_prop rules1 rules2;
    1.21 +val del_rule = remove eq_thm_prop;
    1.22 +fun add_rule th = cons th o del_rule th;
    1.23 +val merge_rules = Library.merge eq_thm_prop;
    1.24  
    1.25  (*weak_eq_thm: ignores variable renaming and (some) type variable renaming*)
    1.26  val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);