--- a/src/ZF/CardinalArith.thy Sat Oct 10 22:44:57 2015 +0200
+++ b/src/ZF/CardinalArith.thy Sat Oct 10 22:50:05 2015 +0200
@@ -12,12 +12,12 @@
"InfCard(i) == Card(i) & nat \<le> i"
definition
- cmult :: "[i,i]=>i" (infixl "|*|" 70) where
- "i |*| j == |i*j|"
+ cmult :: "[i,i]=>i" (infixl "\<otimes>" 70) where
+ "i \<otimes> j == |i*j|"
definition
- cadd :: "[i,i]=>i" (infixl "|+|" 65) where
- "i |+| j == |i+j|"
+ cadd :: "[i,i]=>i" (infixl "\<oplus>" 65) where
+ "i \<oplus> j == |i+j|"
definition
csquare_rel :: "i=>i" where
@@ -39,10 +39,6 @@
of @{term K}\<close>
"csucc(K) == \<mu> L. Card(L) & K<L"
-notation (xsymbols)
- cadd (infixl "\<oplus>" 65) and
- cmult (infixl "\<otimes>" 70)
-
lemma Card_Union [simp,intro,TC]:
assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))"