# HG changeset patch
# User wenzelm
# Date 909669970 -3600
# Node ID 5c0aa825c18e0951b2926ad1725439a266b1b24a
# Parent  3bcc29d0c783f08dcadf214715d8c7722e86ac2e
shyps note for prim. rules;

diff -r 3bcc29d0c783 -r 5c0aa825c18e doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Thu Oct 29 15:05:42 1998 +0100
+++ b/doc-src/Ref/thm.tex	Thu Oct 29 15:06:10 1998 +0100
@@ -285,7 +285,7 @@
 \end{ttdescription}
 
 
-\subsection{*Sort hypotheses} 
+\subsection{*Sort hypotheses} \label{sec:sort-hyps}
 \index{sort hypotheses}
 \begin{ttbox} 
 force_strip_shyps : bool ref \hfill{\bf initially true}
@@ -383,6 +383,14 @@
 to make a signature for the conclusion.  This fails if the signatures are
 incompatible. 
 
+\medskip
+
+The following presentation of primitive rules ignores sort
+hypotheses\index{sort hypotheses} (see also \S\ref{sec:sort-hyps}).  These are
+handled transparently by the logic implementation.
+
+\bigskip
+
 \index{meta-implication}
 The {\bf implication} rules are $({\Imp}I)$
 and $({\Imp}E)$: