src/ZF/Ordinal.thy
changeset 1401 0c439768f45c
parent 852 664052e3cf66
child 1478 2b8c2a7547ab
--- a/src/ZF/Ordinal.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Ordinal.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,11 +8,11 @@
 
 Ordinal = WF + Bool + "simpdata" + "equalities" +
 consts
-  Memrel      	:: "i=>i"
-  Transset,Ord  :: "i=>o"
-  "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
-  "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
-  Limit         :: "i=>o"
+  Memrel      	:: i=>i
+  Transset,Ord  :: i=>o
+  "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
+  "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
+  Limit         :: i=>o
 
 translations
   "x le y"      == "x < succ(y)"