src/HOL/Library/Function_Algebras.thy
changeset 54230 b1d955791529
parent 51489 f738e6dbd844
child 56828 08041569357e
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -83,10 +83,10 @@
     1.4  
     1.5  instance "fun" :: (type, group_add) group_add
     1.6    by default
     1.7 -    (simp_all add: fun_eq_iff diff_minus)
     1.8 +    (simp_all add: fun_eq_iff)
     1.9  
    1.10  instance "fun" :: (type, ab_group_add) ab_group_add
    1.11 -  by default (simp_all add: diff_minus)
    1.12 +  by default simp_all
    1.13  
    1.14  
    1.15  text {* Multiplicative structures *}