# HG changeset patch
# User nipkow
# Date 1044628614 -3600
# Node ID a4cd9057d2eefd41855e3a2525dac34db8398648
# Parent  f67a53bf63bc5b2500fd03e8ee5b1287af970d51
Removed (*) because of comments

diff -r f67a53bf63bc -r a4cd9057d2ee src/HOL/GroupTheory/Group.thy
--- a/src/HOL/GroupTheory/Group.thy	Fri Feb 07 15:36:12 2003 +0100
+++ b/src/HOL/GroupTheory/Group.thy	Fri Feb 07 15:36:54 2003 +0100
@@ -238,8 +238,7 @@
 
 constdefs 
   ProdGroup :: "[('a,'c) group_scheme, ('b,'d) group_scheme] => ('a*'b) group"
-            (infixr "'(*')" 80)
-  "G (*) G' ==
+  "ProdGroup G G' ==
     (| carrier = carrier G \<times> carrier G',
        sum = (%(x, x') (y, y'). (sum G x y, sum G' x' y')),
        gminus = (%(x, y). (gminus G x, gminus G' y)),