diff -r 428efffe8599 -r b50b8c0eec01 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/upair.thy	Fri Jan 03 15:01:55 1997 +0100
@@ -1,3 +1,21 @@
-(*Dummy theory to document dependencies *)
+(*  Title:      ZF/upair.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Definitions involving unordered pairing
+*)
+
+upair = ZF +
 
-upair = ZF
+defs
+  (* Definite descriptions -- via Replace over the set "1" *)
+  the_def       "The(P)    == Union({y . x:{0}, P(y)})"
+  if_def        "if(P,a,b) == THE z. P & z=a | ~P & z=b"
+
+  (*Set difference; binary union and intersection*)
+  Diff_def      "A - B    == { x:A . ~(x:B) }"
+  Un_def        "A Un  B  == Union(Upair(A,B))"
+  Int_def       "A Int B  == Inter(Upair(A,B))"
+
+end