--- 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)"