# HG changeset patch
# User paulson
# Date 859987722 -7200
# Node ID ac81a17f86f89b24bffd0f0bea2eabe3113443eb
# Parent  ba585d52ea4e7b55e618b1420704b33070327277
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy

diff -r ba585d52ea4e -r ac81a17f86f8 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed Apr 02 15:26:52 1997 +0200
+++ b/src/ZF/ZF.thy	Wed Apr 02 15:28:42 1997 +0200
@@ -196,7 +196,6 @@
      and Powerset Axioms using the following definitions. *)
 
   Collect_def   "Collect(A,P) == {y . x:A, x=y & P(x)}"
-  Inter_def     "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
 
   (*Unordered pairs (Upair) express binary union/intersection and cons;
     set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
@@ -204,6 +203,17 @@
   Upair_def   "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
   cons_def    "cons(a,A) == Upair(a,a) Un A"
 
+  (* Difference, general intersection, binary union and small intersection *)
+
+  Diff_def      "A - B    == { x:A . ~(x:B) }"
+  Inter_def     "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
+  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" *)
+
+  the_def       "The(P)    == Union({y . x:{0}, P(y)})"
+  if_def        "if(P,a,b) == THE z. P & z=a | ~P & z=b"
 
   (* this "symmetric" definition works better than {{a}, {a,b}} *)
   Pair_def      "<a,b>  == {{a,a}, {a,b}}"
diff -r ba585d52ea4e -r ac81a17f86f8 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Wed Apr 02 15:26:52 1997 +0200
+++ b/src/ZF/upair.thy	Wed Apr 02 15:28:42 1997 +0200
@@ -3,19 +3,10 @@
     Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Definitions involving unordered pairing
+Dummy theory, but holds the standard ZF simpset.
+	(This is why the +end is present.)
 *)
 
 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