src/ZF/OrderType.thy
changeset 467 92868dab2939
parent 435 ca5356bd315a
child 753 ec86863e87c8
--- a/src/ZF/OrderType.thy	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/OrderType.thy	Tue Jul 12 18:05:03 1994 +0200
@@ -8,7 +8,7 @@
 The order type of a well-ordering is the least ordinal isomorphic to it.
 *)
 
-OrderType = Order + Ordinal + 
+OrderType = OrderArith + Ordinal + 
 consts
   ordermap  :: "[i,i]=>i"
   ordertype :: "[i,i]=>i"