src/HOL/BNF/BNF_Util.thy
changeset 53560 4b5f42cfa244
parent 51893 596baae88a88
child 54008 b15cfc2864de
     1.1 --- a/src/HOL/BNF/BNF_Util.thy	Thu Sep 12 11:05:19 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Util.thy	Thu Sep 12 11:23:49 2013 +0200
     1.3 @@ -47,16 +47,9 @@
     1.4  lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
     1.5  unfolding bij_def inj_on_def by auto blast
     1.6  
     1.7 -lemma pair_mem_Collect_split:
     1.8 -"(\<lambda>x y. (x, y) \<in> {(x, y). P x y}) = P"
     1.9 -by simp
    1.10 -
    1.11  lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R"
    1.12  by simp
    1.13  
    1.14 -lemma Collect_fst_snd_mem_eq: "{p. (fst p, snd p) \<in> A} = A"
    1.15 -by simp
    1.16 -
    1.17  (* Operator: *)
    1.18  definition "Gr A f = {(a, f a) | a. a \<in> A}"
    1.19