1.1 --- a/src/HOL/BNF/BNF_LFP.thy	Thu Jul 11 11:16:23 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_LFP.thy	Sat Jul 13 13:03:21 2013 +0200
     1.3 @@ -215,16 +215,6 @@
     1.4  lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
     1.5  by auto
     1.6  
     1.7 -lemma If_the_inv_into_in_Func:
     1.8 -  "\<lbrakk>inj_on g C; g ` C \<subseteq> A; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow>
     1.9 -  (\<lambda>i. if i \<in> A then if i \<in> g ` C then the_inv_into C g i else x else undefined) \<in> Func A (B \<union> {x})"
    1.10 -unfolding Func_def by (auto dest: the_inv_into_into)
    1.11 -
    1.12 -lemma If_the_inv_into_f_f:
    1.13 -  "\<lbrakk>inj_on g C; g ` C \<subseteq> A; i \<in> C\<rbrakk> \<Longrightarrow>
    1.14 -  ((\<lambda>i. if i \<in> A then if i \<in> g ` C then the_inv_into C g i else x else undefined) o g) i = id i"
    1.15 -unfolding Func_def by (auto elim: the_inv_into_f_f)
    1.16 -
    1.17  (*helps resolution*)
    1.18  lemma well_order_induct_imp:
    1.19    "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>