author | nipkow |

Mon Jan 01 11:54:36 1996 +0100 (1996-01-01) | |

changeset 1429 | 1f0009009219 |

parent 1428 | 15a69dd0a145 |

child 1430 | 439e1476a7f8 |

Modified non-empty-types warning in HOL.

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}