src/ZF/OrderType.thy
changeset 435 ca5356bd315a
child 467 92868dab2939
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/OrderType.thy	Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,22 @@
+(*  Title: 	ZF/OrderType.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Order types.  
+
+The order type of a well-ordering is the least ordinal isomorphic to it.
+*)
+
+OrderType = Order + Ordinal + 
+consts
+  ordermap  :: "[i,i]=>i"
+  ordertype :: "[i,i]=>i"
+
+rules
+  ordermap_def
+      "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
+
+  ordertype_def "ordertype(A,r) == ordermap(A,r)``A"
+
+end