src/ZF/Cardinal.thy
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*}