--- a/src/ZF/CardinalArith.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/CardinalArith.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,12 +9,12 @@
CardinalArith = Cardinal + OrderArith + Arith + Finite +
consts
- InfCard :: "i=>o"
- "|*|" :: "[i,i]=>i" (infixl 70)
- "|+|" :: "[i,i]=>i" (infixl 65)
- csquare_rel :: "i=>i"
- jump_cardinal :: "i=>i"
- csucc :: "i=>i"
+ InfCard :: i=>o
+ "|*|" :: [i,i]=>i (infixl 70)
+ "|+|" :: [i,i]=>i (infixl 65)
+ csquare_rel :: i=>i
+ jump_cardinal :: i=>i
+ csucc :: i=>i
defs