src/ZF/QPair.thy

--- a/src/ZF/QPair.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/QPair.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -29,7 +29,7 @@
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
   "A <*> B"      => "QSigma(A, _K(B))"
 
-rules
+defs
   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)"