Removed (*) because of comments
authornipkow
Fri Feb 07 15:36:54 2003 +0100 (2003-02-07)
changeset 13809a4cd9057d2ee
parent 13808 f67a53bf63bc
child 13810 c3fbfd472365
Removed (*) because of comments
src/HOL/GroupTheory/Group.thy
     1.1 --- a/src/HOL/GroupTheory/Group.thy	Fri Feb 07 15:36:12 2003 +0100
     1.2 +++ b/src/HOL/GroupTheory/Group.thy	Fri Feb 07 15:36:54 2003 +0100
     1.3 @@ -238,8 +238,7 @@
     1.4  
     1.5  constdefs 
     1.6    ProdGroup :: "[('a,'c) group_scheme, ('b,'d) group_scheme] => ('a*'b) group"
     1.7 -            (infixr "'(*')" 80)
     1.8 -  "G (*) G' ==
     1.9 +  "ProdGroup G G' ==
    1.10      (| carrier = carrier G \<times> carrier G',
    1.11         sum = (%(x, x') (y, y'). (sum G x y, sum G' x' y')),
    1.12         gminus = (%(x, y). (gminus G x, gminus G' y)),