# HG changeset patch
# User wenzelm
# Date 1444510205 -7200
# Node ID 4d9c716e7786e901972fd022969914a1caa21b18
# Parent  045b4d7a53e291410bd1e64a4bf4ef365eea643f
tuned syntax -- more symbols;

diff -r 045b4d7a53e2 -r 4d9c716e7786 src/ZF/CardinalArith.thy
--- 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))"