author paulson Wed, 21 Aug 2002 15:56:37 +0200 changeset 13511 e4b129eaa9c6 parent 13510 0a0f37f9c031 child 13512 80edb859fd24
new proof needed now
```--- a/src/ZF/Constructible/Formula.thy	Wed Aug 21 15:55:59 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Wed Aug 21 15:56:37 2002 +0200
@@ -1008,7 +1008,8 @@
subsubsection{*For L to satisfy Powerset *}

lemma LPow_env_typing:
-     "[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"
+    "[| y : Lset(i); Ord(i); y \<subseteq> X |]
+     ==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
by (auto intro: L_I iff: Lset_succ_lrank_iff)

lemma LPow_in_Lset:
@@ -1018,15 +1019,15 @@
apply (rule LsetI [OF succI1])
apply (intro conjI, clarify)
-apply (rule_tac a=x in UN_I, simp+)
+ apply (rule_tac a=x in UN_I, simp+)
txt{*Now to create the formula @{term "y \<subseteq> X"} *}
apply (rule_tac x="Cons(X,Nil)" in bexI)
apply (rule_tac x="subset_fm(0,1)" in bexI)
apply typecheck
-apply (rule conjI)
+ apply (rule conjI)