| changeset 51489 | f738e6dbd844 |
| parent 50998 | 501200635659 |
| child 51641 | cd05e9fcc63d |
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Mar 23 17:11:06 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Mar 23 20:50:39 2013 +0100 @@ -188,9 +188,6 @@ instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult by default (vector mult_commute) -instance vec :: (ab_semigroup_idem_mult, finite) ab_semigroup_idem_mult - by default (vector mult_idem) - instance vec :: (comm_monoid_mult, finite) comm_monoid_mult by default vector