src/HOL/Power.thy
changeset 61378 3e04c9ca001a
parent 61076 bdc1e2f0a86a
child 61531 ab2e862263e7
     1.1 --- a/src/HOL/Power.thy	Fri Oct 09 19:51:20 2015 +0200
     1.2 +++ b/src/HOL/Power.thy	Fri Oct 09 20:26:03 2015 +0200
     1.3 @@ -34,9 +34,6 @@
     1.4  notation (latex output)
     1.5    power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
     1.6  
     1.7 -notation (HTML output)
     1.8 -  power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
     1.9 -
    1.10  text \<open>Special syntax for squares.\<close>
    1.11  
    1.12  abbreviation (xsymbols)
    1.13 @@ -46,9 +43,6 @@
    1.14  notation (latex output)
    1.15    power2  ("(_\<^sup>2)" [1000] 999)
    1.16  
    1.17 -notation (HTML output)
    1.18 -  power2  ("(_\<^sup>2)" [1000] 999)
    1.19 -
    1.20  end
    1.21  
    1.22  context monoid_mult