added add_rules, del_rules;
authorwenzelm
Mon Sep 04 21:18:28 2000 +0200 (2000-09-04)
changeset 9829bf49c3796599
parent 9828 1d8bc4f1833e
child 9830 e4ad74159b43
added add_rules, del_rules;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Mon Sep 04 18:38:53 2000 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Sep 04 21:18:28 2000 +0200
     1.3 @@ -99,6 +99,8 @@
     1.4    val tag_internal      : 'a attribute
     1.5    val has_internal	: tag list -> bool
     1.6    val compose_single    : thm * int * thm -> thm
     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 norm_hhf_eq	: thm
    1.11    val triv_goal         : thm
    1.12 @@ -426,11 +428,15 @@
    1.13  
    1.14  (*Do the two theorems have the same signature?*)
    1.15  fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
    1.16 -fun merge_rules (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
    1.17  
    1.18  (*Useful "distance" function for BEST_FIRST*)
    1.19  val size_of_thm = size_of_term o #prop o rep_thm;
    1.20  
    1.21 +(*maintain lists of theorems --- preserving canonical order*)
    1.22 +val add_rules = Library.generic_extend Thm.eq_thm I I;
    1.23 +fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
    1.24 +fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2;
    1.25 +
    1.26  
    1.27  (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
    1.28      (some) type variable renaming **)