added add_rule, del_rule;
authorwenzelm
Wed Dec 05 03:09:21 2001 +0100 (2001-12-05)
changeset 12373704e50ab65af
parent 12372 cd3a09c7dac9
child 12374 59874c94d0aa
added add_rule, del_rule;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Wed Dec 05 03:07:44 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Dec 05 03:09:21 2001 +0100
     1.3 @@ -101,6 +101,8 @@
     1.4    val close_derivation: thm -> thm
     1.5    val local_standard: thm -> thm
     1.6    val compose_single: thm * int * thm -> thm
     1.7 +  val add_rule: thm -> thm list -> thm list
     1.8 +  val del_rule: thm -> thm list -> thm list
     1.9    val add_rules: thm list -> thm list -> thm list
    1.10    val del_rules: thm list -> thm list -> thm list
    1.11    val merge_rules: thm list * thm list -> thm list
    1.12 @@ -490,6 +492,8 @@
    1.13  (*maintain lists of theorems --- preserving canonical order*)
    1.14  fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
    1.15  fun add_rules rs rules = rs @ del_rules rs rules;
    1.16 +val del_rule = del_rules o single;
    1.17 +val add_rule = add_rules o single;
    1.18  fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2;
    1.19  
    1.20