src/HOL/Library/Groups_Big_Fun.thy
changeset 61378 3e04c9ca001a
parent 60500 903bb1495239
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Fri Oct 09 19:51:20 2015 +0200
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Fri Oct 09 20:26:03 2015 +0200
     1.3 @@ -242,9 +242,6 @@
     1.4    "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
     1.5  syntax (xsymbols)
     1.6    "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
     1.7 -syntax (HTML output)
     1.8 -  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
     1.9 -
    1.10  translations
    1.11    "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
    1.12  
    1.13 @@ -318,9 +315,6 @@
    1.14    "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
    1.15  syntax (xsymbols)
    1.16    "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
    1.17 -syntax (HTML output)
    1.18 -  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
    1.19 -
    1.20  translations
    1.21    "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
    1.22