src/Pure/drule.ML
changeset 13650 31bd2a8cdbe2
parent 13606 2f121149acfe
child 13659 3cf622f6b0b2
     1.1 --- a/src/Pure/drule.ML	Tue Oct 15 15:37:57 2002 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Oct 17 10:52:59 2002 +0200
     1.3 @@ -501,7 +501,10 @@
     1.4  
     1.5  (** theorem equality **)
     1.6  
     1.7 +(*True if the two theorems have the same signature.*)
     1.8  val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
     1.9 +
    1.10 +(*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
    1.11  val eq_thm_prop = op aconv o pairself Thm.prop_of;
    1.12  
    1.13  (*Useful "distance" function for BEST_FIRST*)