src/HOL/Power.thy

--- a/src/HOL/Power.thy	Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Power.thy	Fri Oct 09 20:26:03 2015 +0200
@@ -34,9 +34,6 @@
 notation (latex output)
   power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
 
-notation (HTML output)
-  power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
-
 text \<open>Special syntax for squares.\<close>
 
 abbreviation (xsymbols)
@@ -46,9 +43,6 @@
 notation (latex output)
   power2  ("(_\<^sup>2)" [1000] 999)
 
-notation (HTML output)
-  power2  ("(_\<^sup>2)" [1000] 999)
-
 end
 
 context monoid_mult