# HG changeset patch
# User paulson
# Date 1030012121 -7200
# Node ID cc3bbaf1b8d3c8faae21e0bcd3a40699588acf2b
# Parent  b9e14471629c66fb13cd6dac542a57d1a68cbda7
tweaked

diff -r b9e14471629c -r cc3bbaf1b8d3 src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Wed Aug 21 15:57:24 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Thu Aug 22 12:28:41 2002 +0200
@@ -253,10 +253,10 @@
     "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z[M]. upair(M,x,y,z))"
 
   Union_ax :: "(i=>o) => o"
-    "Union_ax(M) == \<forall>x[M]. (\<exists>z[M]. big_union(M,x,z))"
+    "Union_ax(M) == \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)"
 
   power_ax :: "(i=>o) => o"
-    "power_ax(M) == \<forall>x[M]. (\<exists>z[M]. powerset(M,x,z))"
+    "power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
 
   univalent :: "[i=>o, i, [i,i]=>o] => o"
     "univalent(M,A,P) == 
@@ -265,17 +265,16 @@
   replacement :: "[i=>o, [i,i]=>o] => o"
     "replacement(M,P) == 
       \<forall>A[M]. univalent(M,A,P) -->
-      (\<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)))"
+      (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)"
 
   strong_replacement :: "[i=>o, [i,i]=>o] => o"
     "strong_replacement(M,P) == 
       \<forall>A[M]. univalent(M,A,P) -->
-      (\<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))))"
+      (\<exists>Y[M]. \<forall>b[M]. b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))"
 
   foundation_ax :: "(i=>o) => o"
     "foundation_ax(M) == 
-	\<forall>x[M]. (\<exists>y\<in>x. M(y))
-                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
+	\<forall>x[M]. (\<exists>y\<in>x. M(y)) --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
 
 
 subsection{*A trivial consistency proof for $V_\omega$ *}