small type annotation fix
authorhaftmann
Thu Apr 06 16:10:22 2006 +0200 (2006-04-06)
changeset 1934573439b467e75
parent 19344 b4e00947c8a1
child 19346 c4c003abd830
small type annotation fix
src/HOL/ex/Classpackage.thy
     1.1 --- a/src/HOL/ex/Classpackage.thy	Thu Apr 06 16:09:54 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Thu Apr 06 16:10:22 2006 +0200
     1.3 @@ -302,8 +302,8 @@
     1.4  
     1.5  instance group_prod_def: (group, group) * :: group
     1.6    mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in
     1.7 -              (x1 \<otimes> y1, x2 \<otimes> y2))"
     1.8 -  mult_one_def: "\<one> == (\<one>, \<one>)"
     1.9 +              ((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))"
    1.10 +  mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)"
    1.11    mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
    1.12  by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl)
    1.13