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.5  by (simp add: sats_Or_iff)
     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.10 -by (simp add: sats_Forall_iff) 
    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)
    1.31   apply (simp add: Vfrom_0) 
    1.32  apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)