author paulson Wed Aug 21 15:56:37 2002 +0200 (2002-08-21) changeset 13511 e4b129eaa9c6 parent 13510 0a0f37f9c031 child 13512 80edb859fd24
new proof needed now
```     1.1 --- a/src/ZF/Constructible/Formula.thy	Wed Aug 21 15:55:59 2002 +0200
1.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Aug 21 15:56:37 2002 +0200
1.3 @@ -1008,7 +1008,8 @@
1.4  subsubsection{*For L to satisfy Powerset *}
1.5
1.6  lemma LPow_env_typing:
1.7 -     "[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"
1.8 +    "[| y : Lset(i); Ord(i); y \<subseteq> X |]
1.9 +     ==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
1.10  by (auto intro: L_I iff: Lset_succ_lrank_iff)
1.11
1.12  lemma LPow_in_Lset:
1.13 @@ -1018,15 +1019,15 @@
1.14  apply (rule LsetI [OF succI1])
1.16  apply (intro conjI, clarify)
1.17 -apply (rule_tac a=x in UN_I, simp+)
1.18 + apply (rule_tac a=x in UN_I, simp+)
1.19  txt{*Now to create the formula @{term "y \<subseteq> X"} *}
1.20  apply (rule_tac x="Cons(X,Nil)" in bexI)
1.21   apply (rule_tac x="subset_fm(0,1)" in bexI)
1.22    apply typecheck
1.23 -apply (rule conjI)
1.24 + apply (rule conjI)
1.25  apply (simp add: succ_Un_distrib [symmetric])
1.26  apply (rule equality_iffI)
1.27 -apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing])
1.28 +apply (simp add: Transset_UN [OF Transset_Lset] LPow_env_typing)
1.29  apply (auto intro: L_I iff: Lset_succ_lrank_iff)
1.30  done
1.31
```