# HG changeset patch
# User traytel
# Date 1378977829 -7200
# Node ID 4b5f42cfa24456e0c4f5c82d4ed4aa3601e81c54
# Parent  3858246c7c8f80f9afe6e0b694884dab7eade5ac
removed unused/inlinable theorems

diff -r 3858246c7c8f -r 4b5f42cfa244 src/HOL/BNF/BNF_Def.thy
--- a/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:05:19 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
@@ -110,10 +110,6 @@
 lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
 unfolding Grp_def o_def by auto
 
-lemma wpull_Grp:
-"wpull (Collect (split (Grp A f))) A (f ` A) f id fst snd"
-unfolding wpull_def Grp_def by auto
-
 definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
 
 lemma pick_middlep:
diff -r 3858246c7c8f -r 4b5f42cfa244 src/HOL/BNF/BNF_Util.thy
--- a/src/HOL/BNF/BNF_Util.thy	Thu Sep 12 11:05:19 2013 +0200
+++ b/src/HOL/BNF/BNF_Util.thy	Thu Sep 12 11:23:49 2013 +0200
@@ -47,16 +47,9 @@
 lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
 unfolding bij_def inj_on_def by auto blast
 
-lemma pair_mem_Collect_split:
-"(\<lambda>x y. (x, y) \<in> {(x, y). P x y}) = P"
-by simp
-
 lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R"
 by simp
 
-lemma Collect_fst_snd_mem_eq: "{p. (fst p, snd p) \<in> A} = A"
-by simp
-
 (* Operator: *)
 definition "Gr A f = {(a, f a) | a. a \<in> A}"
 
diff -r 3858246c7c8f -r 4b5f42cfa244 src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Sep 12 11:05:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Sep 12 11:23:49 2013 +0200
@@ -102,7 +102,7 @@
   rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
     @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
   unfold_thms_tac ctxt (srel_def ::
-    @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
+    @{thms pair_collapse Collect_mem_eq mem_Collect_eq prod.cases fst_conv snd_conv
       split_conv}) THEN
   rtac refl 1;