--- a/src/ZF/ZF.thy Sun Jun 06 18:36:36 2004 +0200
+++ b/src/ZF/ZF.thy Tue Jun 08 16:22:30 2004 +0200
@@ -36,8 +36,7 @@
RepFun :: "[i, i => i] => i"
Collect :: "[i, i => o] => i"
-
-text {*Descriptions *}
+text{*Definite descriptions -- via Replace over the set "1"*}
consts
The :: "(i => o) => i" (binder "THE " 10)
If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10)
@@ -49,7 +48,6 @@
"if(P,a,b)" => "If(P,a,b)"
-
text {*Finite Sets *}
consts
Upair :: "[i, i] => i"
@@ -227,6 +225,7 @@
replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==>
b \<in> PrimReplace(A,P) <-> (\<exists>x\<in>A. P(x,b))"
+
defs
(* Derived form of replacement, restricting P to its functional part.
@@ -258,8 +257,7 @@
Un_def: "A Un B == Union(Upair(A,B))"
Int_def: "A Int B == Inter(Upair(A,B))"
- (* Definite descriptions -- via Replace over the set "1" *)
-
+ (* definite descriptions *)
the_def: "The(P) == Union({y . x \<in> {0}, P(y)})"
if_def: "if(P,a,b) == THE z. P & z=a | ~P & z=b"