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