# HG changeset patch
# User nipkow
# Date 820493676 -3600
# Node ID 1f0009009219062d470f806e36905f9c2d668eff
# Parent  15a69dd0a145c957dbdbf29eb9dc2a3121d7ada8
Modified non-empty-types warning in HOL.

diff -r 15a69dd0a145 -r 1f0009009219 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Thu Dec 28 12:37:57 1995 +0100
+++ b/doc-src/Logics/HOL.tex	Mon Jan 01 11:54:36 1996 +0100
@@ -1259,7 +1259,7 @@
 described elsewhere.
 \begin{warn}
   Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
-  unsound~\cite[\S7]{paulson-COLOG}.
+  unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.
 \end{warn}
 A \bfindex{type definition} identifies the new type with a subset of an
 existing type. More precisely, the new type is defined by exhibiting an
@@ -1346,6 +1346,7 @@
 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
 declaring the type and its operations and by stating the desired axioms, you
 should make sure the type has a non-empty model. You must also have a clause
+\par
 \begin{ttbox}
 arities \(ty\): (term,\(\dots\),term)term
 \end{ttbox}