# HG changeset patch
# User wenzelm
# Date 1728504012 -7200
# Node ID e66172629fccdd8485ed7bff1df481baa4303fa8
# Parent  d74e53f674748fd7c88795fd0e180fcaa515f0de
uniform \<Sum> and \<Prod> syntax, following d10fafeb93c0;

diff -r d74e53f67474 -r e66172629fcc src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Oct 09 14:12:56 2024 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Oct 09 22:00:12 2024 +0200
@@ -1415,8 +1415,8 @@
 sublocale prod: comm_monoid_set times 1
   defines prod = prod.F and prod' = prod.G ..
 
-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"
+abbreviation Prod (\<open>\<Prod>\<close>)
+  where "\<Prod> \<equiv> prod (\<lambda>x. x)"
 
 end