--- 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)$: