src/HOL/BNF/BNF_Def.thy
changeset 52659 58b87aa4dc3b
parent 52635 4f84b730c489
child 52660 7f7311d04727
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Mon Jul 15 11:29:19 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Mon Jul 15 14:23:51 2013 +0200
     1.3 @@ -171,9 +171,6 @@
     1.4  lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
     1.5  by auto
     1.6  
     1.7 -lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
     1.8 -unfolding o_def fun_eq_iff by simp
     1.9 -
    1.10  lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
    1.11    by auto
    1.12