src/ZF/Constructible/Formula.thy
 changeset 13535 007559e981c7 parent 13511 e4b129eaa9c6 child 13634 99a593b49b04
```     1.1 --- a/src/ZF/Constructible/Formula.thy	Tue Aug 27 11:09:33 2002 +0200
1.2 +++ b/src/ZF/Constructible/Formula.thy	Tue Aug 27 11:09:35 2002 +0200
1.3 @@ -164,11 +164,6 @@
1.4         ==> (P | Q) <-> sats(A, Or(p,q), env)"
1.6
1.7 -lemma imp_iff_sats:
1.8 -      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
1.9 -       ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
1.11 -
1.12  lemma iff_iff_sats:
1.13        "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
1.14         ==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
1.15 @@ -819,8 +814,6 @@
1.16  apply (blast intro: doubleton_in_Lset)
1.17  done
1.18
1.19 -lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
1.20 -
1.21  lemma singleton_in_LLimit:
1.22      "[| a: Lset(i);  Limit(i) |] ==> {a} : Lset(i)"
1.23  apply (erule Limit_LsetE, assumption)
1.24 @@ -974,7 +967,7 @@
1.25  done
1.26
1.27  text{*Kunen's VI, 1.12 *}
1.28 -lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
1.29 +lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
1.30  apply (erule nat_induct)