src/HOL/ex/Classpackage.thy
changeset 19951 d58e2c564100
parent 19933 16a5037f2d25
child 19958 fc4ac94f03e0
     1.1 --- a/src/HOL/ex/Classpackage.thy	Tue Jun 27 10:09:39 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Jun 27 10:09:44 2006 +0200
     1.3 @@ -304,7 +304,7 @@
     1.4    mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in
     1.5                ((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))"
     1.6    mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)"
     1.7 -  mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
     1.8 +  mult_inv_def: "\<div> x == let (x1::'a::group, x2::'b::group) = x in (\<div> x1, \<div> x2)"
     1.9  by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
    1.10  
    1.11  instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm