src/HOL/Library/Function_Algebras.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 46575 f1e387195a56
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Mon Sep 13 11:13:15 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 ext_iff)
     1.8 +qed (simp_all add: plus_fun_def fun_eq_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 ext_iff)
    1.17 +qed (simp add: zero_fun_def one_fun_def fun_eq_iff)
    1.18  
    1.19  
    1.20  text {* Ring structures *}