src/HOL/Hilbert_Choice.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 39900 549c00e0e89b
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4  qed
     1.5  
     1.6  lemma inj_iff: "(inj f) = (inv f o f = id)"
     1.7 -apply (simp add: o_def ext_iff)
     1.8 +apply (simp add: o_def fun_eq_iff)
     1.9  apply (blast intro: inj_on_inverseI inv_into_f_f)
    1.10  done
    1.11  
    1.12 @@ -178,7 +178,7 @@
    1.13  by (simp add: inj_on_inv_into surj_range)
    1.14  
    1.15  lemma surj_iff: "(surj f) = (f o inv f = id)"
    1.16 -apply (simp add: o_def ext_iff)
    1.17 +apply (simp add: o_def fun_eq_iff)
    1.18  apply (blast intro: surjI surj_f_inv_f)
    1.19  done
    1.20