src/Pure/drule.ML
changeset 9829 bf49c3796599
parent 9554 1b0f02abbde8
child 9862 96138f29545e
equal deleted inserted replaced
9828:1d8bc4f1833e 9829:bf49c3796599
    97   val tag_lemma         : 'a attribute
    97   val tag_lemma         : 'a attribute
    98   val tag_assumption    : 'a attribute
    98   val tag_assumption    : 'a attribute
    99   val tag_internal      : 'a attribute
    99   val tag_internal      : 'a attribute
   100   val has_internal	: tag list -> bool
   100   val has_internal	: tag list -> bool
   101   val compose_single    : thm * int * thm -> thm
   101   val compose_single    : thm * int * thm -> thm
       
   102   val add_rules		: thm list -> thm list -> thm list
       
   103   val del_rules		: thm list -> thm list -> thm list
   102   val merge_rules	: thm list * thm list -> thm list
   104   val merge_rules	: thm list * thm list -> thm list
   103   val norm_hhf_eq	: thm
   105   val norm_hhf_eq	: thm
   104   val triv_goal         : thm
   106   val triv_goal         : thm
   105   val rev_triv_goal     : thm
   107   val rev_triv_goal     : thm
   106   val freeze_all        : thm -> thm
   108   val freeze_all        : thm -> thm
   424 
   426 
   425 (** theorem equality **)
   427 (** theorem equality **)
   426 
   428 
   427 (*Do the two theorems have the same signature?*)
   429 (*Do the two theorems have the same signature?*)
   428 fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
   430 fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
   429 fun merge_rules (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
       
   430 
   431 
   431 (*Useful "distance" function for BEST_FIRST*)
   432 (*Useful "distance" function for BEST_FIRST*)
   432 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 
       
   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);
       
   438 fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2;
   433 
   439 
   434 
   440 
   435 (** 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
   436     (some) type variable renaming **)
   442     (some) type variable renaming **)
   437 
   443