changeset 14565 | c6dc17aab88a |
parent 14153 | 76a6ba67bd15 |
child 14883 | ca000a495448 |
--- a/src/ZF/Cardinal.thy Wed Apr 14 13:28:46 2004 +0200 +++ b/src/ZF/Cardinal.thy Wed Apr 14 14:13:05 2004 +0200 @@ -39,6 +39,10 @@ "lesspoll" :: "[i,i] => o" (infixl "\<prec>" 50) "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10) +syntax (HTML output) + "eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50) + "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10) + subsection{*The Schroeder-Bernstein Theorem*} text{*See Davey and Priestly, page 106*}