| changeset 59815 | cce82e360c2f |
| parent 58881 | b9556a055632 |
| child 60500 | 903bb1495239 |
--- a/src/HOL/Library/Function_Algebras.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/Library/Function_Algebras.thy Mon Mar 23 19:05:14 2015 +0100 @@ -71,7 +71,7 @@ by default (simp add: fun_eq_iff add.commute) instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add - by default simp + by default (simp_all add: fun_eq_iff diff_diff_eq) instance "fun" :: (type, monoid_add) monoid_add by default (simp_all add: fun_eq_iff)