src/HOL/BNF/BNF_Def.thy
changeset 53560 4b5f42cfa244
parent 52986 7f7bbeb16538
child 53561 92bcac4f9ac9
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:05:19 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
     1.3 @@ -110,10 +110,6 @@
     1.4  lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
     1.5  unfolding Grp_def o_def by auto
     1.6  
     1.7 -lemma wpull_Grp:
     1.8 -"wpull (Collect (split (Grp A f))) A (f ` A) f id fst snd"
     1.9 -unfolding wpull_def Grp_def by auto
    1.10 -
    1.11  definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
    1.12  
    1.13  lemma pick_middlep: