--- a/src/HOL/Groups_Big.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Groups_Big.thy Fri Oct 09 20:26:03 2015 +0200
@@ -493,8 +493,6 @@
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_./ _)" [0, 51, 10] 10)
syntax (xsymbols)
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
translations -- \<open>Beware of argument permutation!\<close>
"SUM i:A. b" == "CONST setsum (%i. b) A"
@@ -507,8 +505,6 @@
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
syntax (xsymbols)
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
-syntax (HTML output)
- "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
translations
"SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
@@ -1077,8 +1073,6 @@
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD _:_./ _)" [0, 51, 10] 10)
syntax (xsymbols)
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
translations -- \<open>Beware of argument permutation!\<close>
"PROD i:A. b" == "CONST setprod (%i. b) A"
@@ -1091,8 +1085,6 @@
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
syntax (xsymbols)
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
-syntax (HTML output)
- "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
translations
"PROD x|P. t" => "CONST setprod (%x. t) {x. P}"