--- a/src/HOL/Library/Groups_Big_Fun.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sun Aug 25 21:10:01 2024 +0200
@@ -202,6 +202,8 @@
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _. _)" [0, 10] 10)
syntax
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_. _)" [0, 10] 10)
+syntax_consts
+ "_Sum_any" \<rightleftharpoons> Sum_any
translations
"\<Sum>a. b" \<rightleftharpoons> "CONST Sum_any (\<lambda>a. b)"
@@ -255,6 +257,8 @@
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _. _)" [0, 10] 10)
syntax
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_. _)" [0, 10] 10)
+syntax_consts
+ "_Prod_any" == Prod_any
translations
"\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"