# HG changeset patch
# User paulson
# Date 844074254 -7200
# Node ID e8d52d05530a2d911970dcc9d4add669cb1782a3
# Parent  8de7a0ab463bed80f59f0919a67a61513af0e1e6
Improved discussion of shyps thanks to Markus Wenzel

diff -r 8de7a0ab463b -r e8d52d05530a doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Mon Sep 30 10:59:47 1996 +0200
+++ b/doc-src/Ref/thm.tex	Mon Sep 30 11:04:14 1996 +0200
@@ -260,23 +260,30 @@
 causes sort hypotheses to be deleted, printing a warning.
 \end{ttdescription}
 
-A sort is {\em empty\/} if there are no types having that sort.  If a theorem
-contain a type variable whose sort is empty, then that theorem has no
-instances.  In effect, it asserts nothing.  But what if it is used to prove
-another theorem that no longer involves that sort?  The latter theorem holds
-only if the sort is non-empty.
+Isabelle's type variables are decorated with sorts, constraining them to
+certain ranges of types.  This has little impact when sorts only serve for
+syntactic classification of types --- for example, FOL distinguishes between
+terms and other types.  But when type classes are introduced through axioms,
+this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
+a type belonging to it because certain axioms are unsatisfiable.
+
+If a theorem contain a type variable whose sort is empty, then that theorem
+has no instances.  In effect, it asserts nothing.  But what if it is used to
+prove another theorem that no longer involves that sort?  The latter theorem
+holds only if the sort is non-empty.
 
-Theorems are therefore subject to sort hypotheses, which express that certain
-sorts are non-empty.  The {\tt shyps} field is a list of sorts occurring in
-type variables.  The list includes all sorts from the current theorem (the
-{\tt prop} and {\tt hyps} fields).  It also includes sorts used in the
-theorem's proof --- so-called {\em dangling\/} sort constraints.  These are
-the critical ones that must be non-empty in order for the proof to be valid.
-
-Isabelle removes sorts from the {\tt shyps} field whenever
-non-emptiness holds.  Because its current implementation is highly incomplete,
-the flag shown above is available.  Setting it to true (the default) allows
-existing proofs to run.
+Therefore, Isabelle's theorems carry around sort hypotheses. The {\tt
+shyps} field is a list of sorts occurring in type variables in the current
+{\tt prop} and {\tt hyps} fields.  It may also includes sorts used in the
+theorem's proof that no longer appear in the {\tt prop} or {\tt hyps}
+fields --- so-called {\em dangling\/} sort constraints. These are the
+critical ones, asserting non-emptiness of the corresponding sorts.
+ 
+Isabelle tries to remove extraneous sorts from the {\tt shyps} field whenever
+non-emptiness can be established by looking at the theorem's signature: from
+the {\tt arities} information, etc.  Because its current implementation is
+highly incomplete, the flag shown above is available.  Setting it to true (the
+default) allows existing proofs to run.
 
 
 \subsection{Tracing flags for unification}