src/HOL/Library/Groups_Big_Fun.thy

 
 syntax
   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
 syntax (xsymbols)
   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
-syntax (HTML output)
-  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
-
 translations
   "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
 
 lemma Sum_any_left_distrib:
   fixes r :: "'a :: semiring_0"

 
 syntax
   "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
 syntax (xsymbols)
   "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
-syntax (HTML output)
-  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
-
 translations
   "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
 
 lemma Prod_any_zero:
   fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"