src/ZF/Nat.thy
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"