src/ZF/Ordinal.thy
changeset 61378 3e04c9ca001a
parent 60770 240563fbf41d
child 61397 6204c86280ff
--- a/src/ZF/Ordinal.thy	Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/Ordinal.thy	Fri Oct 09 20:26:03 2015 +0200
@@ -34,9 +34,6 @@
 notation (xsymbols)
   le  (infixl "\<le>" 50)
 
-notation (HTML output)
-  le  (infixl "\<le>" 50)
-
 
 subsection\<open>Rules for Transset\<close>