changeset 13504 | 59066e97b551 |
parent 13503 | d93f41fe35d2 |
child 13505 | 52a16cb7fefb |
--- 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)