diff -r 685499c73215 -r d16629fd0f95 src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Mon Jul 08 17:24:07 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Mon Jul 08 17:51:56 2002 +0200
@@ -130,6 +130,11 @@
        ==> (x=y) <-> sats(A, Equal(i,j), env)" 
 by (simp add: satisfies.simps)
 
+lemma not_iff_sats:
+      "[| P <-> sats(A,p,env); env \<in> list(A)|]
+       ==> (~P) <-> sats(A, Neg(p), env)"
+by simp
+
 lemma conj_iff_sats:
       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
        ==> (P & Q) <-> sats(A, And(p,q), env)"
@@ -165,6 +170,10 @@
        ==> (\<exists>x\<in>A. P(x)) <-> sats(A, Exists(p), env)"
 by (simp add: sats_Exists_iff) 
 
+lemmas FOL_iff_sats = 
+        mem_iff_sats equal_iff_sats not_iff_sats conj_iff_sats
+        disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats
+        bex_iff_sats
 
 constdefs incr_var :: "[i,i]=>i"
     "incr_var(x,lev) == if x<lev then x else succ(x)"