1.1 --- a/doc-src/Ref/tctical.tex	Mon May 06 09:42:20 2002 +0200
     1.2 +++ b/doc-src/Ref/tctical.tex	Tue May 07 14:24:30 2002 +0200
     1.3 @@ -303,6 +303,7 @@
     1.4  \begin{ttbox} 
     1.5  has_fewer_prems : int -> thm -> bool
     1.6  eq_thm          : thm * thm -> bool
     1.7 +eq_thm_prop     : thm * thm -> bool
     1.8  size_of_thm     : thm -> int
     1.9  \end{ttbox}
    1.10  \begin{ttdescription}
    1.11 @@ -312,9 +313,14 @@
    1.12  be given to the searching tacticals.
    1.13  
    1.14  \item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and
    1.15 -  $thm@2$ are equal.  Both theorems must have identical signatures.  Both
    1.16 -  theorems must have the same conclusions, and the same hypotheses, in the
    1.17 -  same order.  Names of bound variables are ignored.
    1.18 +  $thm@2$ are equal.  Both theorems must have compatible signatures.  Both
    1.19 +  theorems must have the same conclusions, the same hypotheses (in the same
    1.20 +  order), and the same set of sort hypotheses.  Names of bound variables are
    1.21 +  ignored.
    1.22 +  
    1.23 +\item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the
    1.24 +  propositions of $thm@1$ and $thm@2$ are equal.  Names of bound variables are
    1.25 +  ignored.
    1.26  
    1.27  \item[\ttindexbold{size_of_thm} $thm$] 
    1.28  computes the size of $thm$, namely the number of variables, constants and