diff -r 60647586b173 -r 743e8ca36b18 src/HOL/ZF/Helper.thy
--- a/src/HOL/ZF/Helper.thy	Tue Mar 02 20:36:07 2010 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(*  Title:      HOL/ZF/Helper.thy
-    ID:         $Id$
-    Author:     Steven Obua
-
-    Some helpful lemmas that probably will end up elsewhere. 
-*)
-
-theory Helper 
-imports Main
-begin
-
-lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)"
-  apply auto
-  apply (subgoal_tac "P (THE x. P x)")
-  apply blast
-  apply (rule theI)
-  apply auto
-  done
-
-lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)" 
-  by auto
-
-lemma f_x_in_range_f: "f x \<in> range f"
-  by (blast intro: image_eqI)
-
-lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)"
-  by (blast intro: comp_inj_on subset_inj_on)
-
-lemma comp_image_eq: "(g o f) ` x = g ` f ` x"
-  by auto
-  
-end
\ No newline at end of file