src/Pure/drule.ML
changeset 9862 96138f29545e
parent 9829 bf49c3796599
child 10403 2955ee2424ce
equal deleted inserted replaced
9861:b2a6d854d6da 9862:96138f29545e
   431 
   431 
   432 (*Useful "distance" function for BEST_FIRST*)
   432 (*Useful "distance" function for BEST_FIRST*)
   433 val size_of_thm = size_of_term o #prop o rep_thm;
   433 val size_of_thm = size_of_term o #prop o rep_thm;
   434 
   434 
   435 (*maintain lists of theorems --- preserving canonical order*)
   435 (*maintain lists of theorems --- preserving canonical order*)
   436 val add_rules = Library.generic_extend Thm.eq_thm I I;
       
   437 fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
   436 fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
       
   437 fun add_rules rs rules = rs @ del_rules rs rules;
   438 fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2;
   438 fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2;
   439 
   439 
   440 
   440 
   441 (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
   441 (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
   442     (some) type variable renaming **)
   442     (some) type variable renaming **)