src/ZF/Constructible/Formula.thy

 
 lemma disj_iff_sats:
       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
        ==> (P | Q) <-> sats(A, Or(p,q), env)"
 by (simp add: sats_Or_iff)
-
-lemma imp_iff_sats:
-      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
-       ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
-by (simp add: sats_Forall_iff) 
 
 lemma iff_iff_sats:
       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
        ==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
 by (simp add: sats_Forall_iff) 

     "[| a: Lset(i);  b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))"
 apply (unfold Pair_def)
 apply (blast intro: doubleton_in_Lset) 
 done
 
-lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
-
 lemma singleton_in_LLimit:
     "[| a: Lset(i);  Limit(i) |] ==> {a} : Lset(i)"
 apply (erule Limit_LsetE, assumption)
 apply (erule singleton_in_Lset [THEN lt_LsetI])
 apply (blast intro: Limit_has_succ) 

 apply (rule subset_trans [OF DPow_subset_Pow]) 
 apply (rule Pow_mono, blast) 
 done
 
 text{*Kunen's VI, 1.12 *}
-lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
+lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
 apply (erule nat_induct)
  apply (simp add: Vfrom_0) 
 apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) 
 done