--- a/src/ZF/Cardinal.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/ZF/Cardinal.thy Sun Nov 26 18:07:16 2006 +0100
@@ -33,15 +33,16 @@
Card :: "i=>o"
"Card(i) == (i = |i|)"
-syntax (xsymbols)
- "eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50)
- "lepoll" :: "[i,i] => o" (infixl "\<lesssim>" 50)
- "lesspoll" :: "[i,i] => o" (infixl "\<prec>" 50)
- "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
+notation (xsymbols)
+ eqpoll (infixl "\<approx>" 50) and
+ lepoll (infixl "\<lesssim>" 50) and
+ lesspoll (infixl "\<prec>" 50) and
+ Least (binder "\<mu>" 10)
-syntax (HTML output)
- "eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50)
- "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
+notation (HTML output)
+ eqpoll (infixl "\<approx>" 50) and
+ Least (binder "\<mu>" 10)
+
subsection{*The Schroeder-Bernstein Theorem*}
text{*See Davey and Priestly, page 106*}