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, \ep z. \env\list(A). \p\formula. - ep = & z = {x \ A . sats(A, p, Cons(x, env))})" + ep = & z = {x \ A . sats(A, p, Cons(x, env))})" by (insert rep [of A], simp add: Collect_DPow_body_abs)