diff -r 000000000000 -r a5a9c433f639 src/ZF/qpair.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/qpair.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,52 @@
+(*  Title: 	ZF/qpair.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
+structures in ZF.  Does not precisely follow Quine's construction.  Thanks
+to Thomas Forster for suggesting this approach!
+
+W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
+1966.
+*)
+
+QPair = Sum +
+consts
+  QPair     :: "[i, i] => i"               	("<(_;/ _)>")
+  qsplit    :: "[[i,i] => i, i] => i"
+  qfsplit   :: "[[i,i] => o, i] => o"
+  qconverse :: "i => i"
+  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
+  " <*>"    :: "[i, i] => i"         		("(_ <*>/ _)" [81, 80] 80)
+  QSigma    :: "[i, i => i] => i"
+
+  "<+>"     :: "[i,i]=>i"      			(infixr 65)
+  QInl,QInr :: "i=>i"
+  qcase     :: "[i=>i, i=>i, i]=>i"
+
+translations
+  "QSUM x:A. B"  => "QSigma(A, %x. B)"
+
+rules
+  QPair_def       "<a;b> == a+b"
+  qsplit_def      "qsplit(c,p)  ==  THE y. EX a b. p=<a;b> & y=c(a,b)"
+  qfsplit_def     "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
+  qconverse_def   "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
+  QSigma_def      "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
+
+  qsum_def        "A <+> B      == QSigma({0}, %x.A) Un QSigma({1}, %x.B)"
+  QInl_def        "QInl(a)      == <0;a>"
+  QInr_def        "QInr(b)      == <1;b>"
+  qcase_def       "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
+end
+
+ML
+
+(* 'Dependent' type operators *)
+
+val parse_translation =
+  [(" <*>", ndependent_tr "QSigma")];
+
+val print_translation =
+  [("QSigma", dependent_tr' ("@QSUM", " <*>"))];