--- a/src/ZF/upair.thy Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/upair.thy Sun Jul 14 15:14:43 2002 +0200
@@ -18,6 +18,9 @@
setup TypeCheck.setup
declare atomize_ball [symmetric, rulify]
+(*belongs to theory ZF*)
+declare bspec [dest?]
+
(*** Lemmas about power sets ***)
lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *)
@@ -54,6 +57,9 @@
lemma UnI2: "c : B ==> c : A Un B"
by simp
+(*belongs to theory upair*)
+declare UnI1 [elim?] UnI2 [elim?]
+
lemma UnE [elim!]: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"
apply simp
apply blast