
diff -r d93f41fe35d2 -r 59066e97b551 src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Thu Aug 15 21:36:26 2002 +0200
+++ b/src/ZF/Constructible/DPow_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
@@ -204,7 +204,7 @@
    "M(A)
     ==> strong_replacement (M, 
          \<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula.
-                  ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})"
+                  ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})" 
 by (insert rep [of A], simp add: Collect_DPow_body_abs) 
 
 




