src/Pure/drule.ML

--- a/src/Pure/drule.ML	Tue Oct 15 15:37:57 2002 +0200
+++ b/src/Pure/drule.ML	Thu Oct 17 10:52:59 2002 +0200
@@ -501,7 +501,10 @@
 
 (** theorem equality **)
 
+(*True if the two theorems have the same signature.*)
 val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
+
+(*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
 val eq_thm_prop = op aconv o pairself Thm.prop_of;
 
 (*Useful "distance" function for BEST_FIRST*)