# HG changeset patch
# User krauss
# Date 1267548310 -3600
# Node ID 3d105282262ef9023bf588d434d786347d345e2e
# Parent  5d88ffdb290c0d5ae3b9498950ba51c99c7683ce
removed obsolete helper theory

diff -r 5d88ffdb290c -r 3d105282262e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Mar 02 15:39:15 2010 +0100
+++ b/src/HOL/IsaMakefile	Tue Mar 02 17:45:10 2010 +0100
@@ -756,7 +756,7 @@
 
 HOL-ZF: HOL $(LOG)/HOL-ZF.gz
 
-$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy	\
+$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy	\
   ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
 
diff -r 5d88ffdb290c -r 3d105282262e src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Tue Mar 02 15:39:15 2010 +0100
+++ b/src/HOL/ZF/HOLZF.thy	Tue Mar 02 17:45:10 2010 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory HOLZF 
-imports Helper
+imports Main
 begin
 
 typedecl ZF
@@ -298,7 +298,7 @@
   apply (rule_tac x="Fst z" in exI)
   apply (simp add: isOpair_def)
   apply (auto simp add: Fst Snd Opair)
-  apply (rule theI2')
+  apply (rule the1I2)
   apply auto
   apply (drule Fun_implies_PFun)
   apply (drule_tac x="Opair x ya" and y="Opair x yb" in PFun_inj)
@@ -306,7 +306,7 @@
   apply (drule Fun_implies_PFun)
   apply (drule_tac x="Opair x y" and y="Opair x ya" in PFun_inj)
   apply (auto simp add: Fst Snd)
-  apply (rule theI2')
+  apply (rule the1I2)
   apply (auto simp add: Fun_total)
   apply (drule Fun_implies_PFun)
   apply (drule_tac x="Opair a x" and y="Opair a y" in PFun_inj)
diff -r 5d88ffdb290c -r 3d105282262e src/HOL/ZF/Helper.thy
--- a/src/HOL/ZF/Helper.thy	Tue Mar 02 15:39:15 2010 +0100
+++ /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
diff -r 5d88ffdb290c -r 3d105282262e src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Tue Mar 02 15:39:15 2010 +0100
+++ b/src/HOL/ZF/Zet.thy	Tue Mar 02 17:45:10 2010 +0100
@@ -35,7 +35,7 @@
   apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
   apply (simp add: explode_Repl_eq)
   apply (subgoal_tac "explode z = f ` A")
-  apply (simp_all add: comp_image_eq)
+  apply (simp_all add: image_compose)
   done
 
 lemma zet_image_mem:
@@ -56,7 +56,7 @@
     apply (auto simp add: subset injf)
     done
   show ?thesis
-    apply (simp add: zet_def' comp_image_eq[symmetric])
+    apply (simp add: zet_def' image_compose[symmetric])
     apply (rule exI[where x="?w"])
     apply (simp add: injw image_zet_rep Azet)
     done
@@ -108,7 +108,7 @@
 lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
   apply (simp add: zimage_def)
   apply (subst Abs_zet_inverse)
-  apply (simp_all add: comp_image_eq zet_image_mem Rep_zet)
+  apply (simp_all add: image_compose zet_image_mem Rep_zet)
   done
     
 definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where