Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Constructible/DPow_absolute.thy
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)
isabelle