| changeset 51489 | f738e6dbd844 |
| parent 48173 | c6a5a4336edf |
| child 54230 | b1d955791529 |
--- a/src/HOL/Library/Function_Algebras.thy Sat Mar 23 17:11:06 2013 +0100 +++ b/src/HOL/Library/Function_Algebras.thy Sat Mar 23 20:50:39 2013 +0100 @@ -97,9 +97,6 @@ instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult by default (simp add: fun_eq_iff mult.commute) -instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult - by default (simp add: fun_eq_iff) - instance "fun" :: (type, monoid_mult) monoid_mult by default (simp_all add: fun_eq_iff)