src/Pure/drule.ML
changeset 13650 31bd2a8cdbe2
parent 13606 2f121149acfe
child 13659 3cf622f6b0b2
equal deleted inserted replaced
13649:0f562a70c07d 13650:31bd2a8cdbe2
   499       | _ =>   raise THM("COMP", 1, [tha,thb]);
   499       | _ =>   raise THM("COMP", 1, [tha,thb]);
   500 
   500 
   501 
   501 
   502 (** theorem equality **)
   502 (** theorem equality **)
   503 
   503 
       
   504 (*True if the two theorems have the same signature.*)
   504 val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
   505 val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
       
   506 
       
   507 (*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
   505 val eq_thm_prop = op aconv o pairself Thm.prop_of;
   508 val eq_thm_prop = op aconv o pairself Thm.prop_of;
   506 
   509 
   507 (*Useful "distance" function for BEST_FIRST*)
   510 (*Useful "distance" function for BEST_FIRST*)
   508 val size_of_thm = size_of_term o prop_of;
   511 val size_of_thm = size_of_term o prop_of;
   509 
   512