# HG changeset patch
# User traytel
# Date 1460044586 -7200
# Node ID 75ca185db27f90a9ccfc4333f9da611e301767bc
# Parent  52c5a25e0c96ecb0fba9fb5dc188ab66a497b60f
removed duplicate lemma

diff -r 52c5a25e0c96 -r 75ca185db27f src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:56:22 2016 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:56:26 2016 +0200
@@ -43,9 +43,6 @@
 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
   unfolding bij_betw_def by auto
 
-lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
-  unfolding bij_betw_def by auto
-
 lemma f_the_inv_into_f_bij_betw:
   "bij_betw f A B \<Longrightarrow> (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
   unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
diff -r 52c5a25e0c96 -r 75ca185db27f src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Apr 07 17:56:22 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Apr 07 17:56:26 2016 +0200
@@ -169,11 +169,11 @@
     val n = length alg_sets;
     fun set_tac thm =
       EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono},
-        rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE}];
+        rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on}];
     val alg_tac =
       CONJ_WRAP' (fn (set_maps, alg_set) =>
         EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
-          rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
+          rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]},
           rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
       (set_mapss ~~ alg_sets);