src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
changeset 51489 f738e6dbd844
parent 50998 501200635659
child 51641 cd05e9fcc63d
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Mar 23 17:11:06 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Mar 23 20:50:39 2013 +0100
     1.3 @@ -188,9 +188,6 @@
     1.4  instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult
     1.5    by default (vector mult_commute)
     1.6  
     1.7 -instance vec :: (ab_semigroup_idem_mult, finite) ab_semigroup_idem_mult
     1.8 -  by default (vector mult_idem)
     1.9 -
    1.10  instance vec :: (comm_monoid_mult, finite) comm_monoid_mult
    1.11    by default vector
    1.12