Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/CardinalArith.thy
changeset 61401 4d9c716e7786
parent 61394 6142b282b164
child 61798 27f3c10b0b50 
--- 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))"
isabelle