src/HOL/HOLCF/Ssum.thy
changeset 61378 3e04c9ca001a
parent 58880 0baae4311a9f
child 61998 b66d2ca1f907
     1.1 --- a/src/HOL/HOLCF/Ssum.thy	Fri Oct 09 19:51:20 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Ssum.thy	Fri Oct 09 20:26:03 2015 +0200
     1.3 @@ -27,8 +27,6 @@
     1.4  
     1.5  type_notation (xsymbols)
     1.6    ssum  ("(_ \<oplus>/ _)" [21, 20] 20)
     1.7 -type_notation (HTML output)
     1.8 -  ssum  ("(_ \<oplus>/ _)" [21, 20] 20)
     1.9  
    1.10  
    1.11  subsection {* Definitions of constructors *}