--- a/src/HOL/Library/Groups_Big_Fun.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Fri Oct 09 20:26:03 2015 +0200
@@ -242,9 +242,6 @@
"_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)"
@@ -318,9 +315,6 @@
"_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)"