src/HOL/Hilbert_Choice.thy
changeset 44921 58eef4843641
parent 44890 22f665a2e91c
child 45607 16b4f5774621
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -123,7 +123,7 @@
     1.4  by (simp add:inv_into_f_eq)
     1.5  
     1.6  lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
     1.7 -by (blast intro: ext inv_into_f_eq)
     1.8 +  by (blast intro: inv_into_f_eq)
     1.9  
    1.10  text{*But is it useful?*}
    1.11  lemma inj_transfer:
    1.12 @@ -286,7 +286,7 @@
    1.13    hence "?f'' a = a'"
    1.14      using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
    1.15    moreover have "f a = a'" using assms 2 3
    1.16 -    by (auto simp add: inv_into_f_f bij_betw_def)
    1.17 +    by (auto simp add: bij_betw_def)
    1.18    ultimately show "?f'' a = f a" by simp
    1.19  qed
    1.20