doc-src/Ref/tctical.tex

 \index{theorems!size of}
 \index{theorems!equality of}
 \begin{ttbox} 
 has_fewer_prems : int -> thm -> bool
 eq_thm          : thm * thm -> bool
+eq_thm_prop     : thm * thm -> bool
 size_of_thm     : thm -> int
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{has_fewer_prems} $n$ $thm$] 
 reports whether $thm$ has fewer than~$n$ premises.  By currying,
 \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may 
 be given to the searching tacticals.
 
 \item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and
-  $thm@2$ are equal.  Both theorems must have identical signatures.  Both
-  theorems must have the same conclusions, and the same hypotheses, in the
-  same order.  Names of bound variables are ignored.
+  $thm@2$ are equal.  Both theorems must have compatible signatures.  Both
+  theorems must have the same conclusions, the same hypotheses (in the same
+  order), and the same set of sort hypotheses.  Names of bound variables are
+  ignored.
+  
+\item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the
+  propositions of $thm@1$ and $thm@2$ are equal.  Names of bound variables are
+  ignored.
 
 \item[\ttindexbold{size_of_thm} $thm$] 
 computes the size of $thm$, namely the number of variables, constants and
 abstractions in its conclusion.  It may serve as a distance function for 
 \ttindex{BEST_FIRST}.