Modified non-empty-types warning in HOL.
authornipkow
Mon Jan 01 11:54:36 1996 +0100 (1996-01-01)
changeset 14291f0009009219
parent 1428 15a69dd0a145
child 1430 439e1476a7f8
Modified non-empty-types warning in HOL.
doc-src/Logics/HOL.tex
     1.1 --- a/doc-src/Logics/HOL.tex	Thu Dec 28 12:37:57 1995 +0100
     1.2 +++ b/doc-src/Logics/HOL.tex	Mon Jan 01 11:54:36 1996 +0100
     1.3 @@ -1259,7 +1259,7 @@
     1.4  described elsewhere.
     1.5  \begin{warn}
     1.6    Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
     1.7 -  unsound~\cite[\S7]{paulson-COLOG}.
     1.8 +  unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.
     1.9  \end{warn}
    1.10  A \bfindex{type definition} identifies the new type with a subset of an
    1.11  existing type. More precisely, the new type is defined by exhibiting an
    1.12 @@ -1346,6 +1346,7 @@
    1.13  If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
    1.14  declaring the type and its operations and by stating the desired axioms, you
    1.15  should make sure the type has a non-empty model. You must also have a clause
    1.16 +\par
    1.17  \begin{ttbox}
    1.18  arities \(ty\): (term,\(\dots\),term)term
    1.19  \end{ttbox}