# HG changeset patch
# User wenzelm
# Date 1020774270 -7200
# Node ID df7aac8543c92308399338a6fc8cfdf7de938afd
# Parent  66659a4b16f6fff6550c389c7b22629fc9fa2f25
clarified eq_thm;
added eq_thm_prop;

diff -r 66659a4b16f6 -r df7aac8543c9 doc-src/Ref/tctical.tex
--- a/doc-src/Ref/tctical.tex	Mon May 06 09:42:20 2002 +0200
+++ b/doc-src/Ref/tctical.tex	Tue May 07 14:24:30 2002 +0200
@@ -303,6 +303,7 @@
 \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}
@@ -312,9 +313,14 @@
 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