changeset 435 | ca5356bd315a |
parent 124 | 858ab9a9b047 |
child 753 | ec86863e87c8 |
--- a/src/ZF/Nat.thy Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Nat.thy Tue Jun 21 17:20:34 1994 +0200 @@ -1,12 +1,12 @@ -(* Title: ZF/nat.thy +(* Title: ZF/Nat.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge + Copyright 1994 University of Cambridge Natural numbers in Zermelo-Fraenkel Set Theory *) -Nat = Ord + Bool + "mono" + +Nat = Ordinal + Bool + "mono" + consts nat :: "i" nat_case :: "[i, i=>i, i]=>i"