src/HOL/Library/Function_Algebras.thy
changeset 39198 f967a16dfcdd
parent 38642 8fa437809c67
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  qed (simp add: plus_fun_def add.assoc)
     1.5  
     1.6  instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
     1.7 -qed (simp_all add: plus_fun_def expand_fun_eq)
     1.8 +qed (simp_all add: plus_fun_def ext_iff)
     1.9  
    1.10  instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
    1.11  qed (simp add: plus_fun_def add.commute)
    1.12 @@ -106,7 +106,7 @@
    1.13  qed (simp_all add: zero_fun_def times_fun_def)
    1.14  
    1.15  instance "fun" :: (type, zero_neq_one) zero_neq_one proof
    1.16 -qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
    1.17 +qed (simp add: zero_fun_def one_fun_def ext_iff)
    1.18  
    1.19  
    1.20  text {* Ring structures *}