# HG changeset patch
# User traytel
# Date 1392742608 -3600
# Node ID 4394bb0b522b5bfd8e6b142cff8682b7f4b38ea5
# Parent  fd9ea8ae28f6c1c72740a66b08a670bb17363c56
removed not anymore used theorems

diff -r fd9ea8ae28f6 -r 4394bb0b522b src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Tue Feb 18 14:51:26 2014 +0100
+++ b/src/HOL/BNF_GFP.thy	Tue Feb 18 17:56:48 2014 +0100
@@ -51,21 +51,6 @@
 (* Operators: *)
 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
 
-lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
-unfolding Id_on_def by simp
-
-lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
-unfolding Id_on_def by auto
-
-lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
-unfolding Id_on_def by auto
-
-lemma Id_on_UNIV: "Id_on UNIV = Id"
-unfolding Id_on_def by auto
-
-lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
-unfolding Id_on_def by auto
-
 lemma Id_on_Gr: "Id_on A = Gr A id"
 unfolding Id_on_def Gr_def by auto
 
@@ -102,9 +87,6 @@
 lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
 by force
 
-lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
-by auto
-
 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
 unfolding fun_eq_iff by auto
 
@@ -114,9 +96,6 @@
 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
 unfolding Gr_def Grp_def fun_eq_iff by auto
 
-lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
-unfolding fun_eq_iff by auto
-
 definition relImage where
 "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"