src/HOL/Groups_Big.thy

--- a/src/HOL/Groups_Big.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Groups_Big.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -1415,7 +1415,7 @@
 sublocale prod: comm_monoid_set times 1
   defines prod = prod.F and prod' = prod.G ..
 
-abbreviation Prod (\<open>\<Prod>_\<close> [1000] 999)
+abbreviation Prod (\<open>(\<open>open_block notation=\<open>prefix \<Prod>\<close>\<close>\<Prod>_)\<close> [1000] 999)
   where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
 
 end