# 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 \ i" definition - cmult :: "[i,i]=>i" (infixl "|*|" 70) where - "i |*| j == |i*j|" + cmult :: "[i,i]=>i" (infixl "\" 70) where + "i \ j == |i*j|" definition - cadd :: "[i,i]=>i" (infixl "|+|" 65) where - "i |+| j == |i+j|" + cadd :: "[i,i]=>i" (infixl "\" 65) where + "i \ j == |i+j|" definition csquare_rel :: "i=>i" where @@ -39,10 +39,6 @@ of @{term K}\ "csucc(K) == \ L. Card(L) & K" 65) and - cmult (infixl "\" 70) - lemma Card_Union [simp,intro,TC]: assumes A: "\x. x\A \ Card(x)" shows "Card(\(A))"