# HG changeset patch
# User lcp
# Date 799506401 -7200
# Node ID 01379c46ad2df6720c0f5340dae09fbab7f1601c
# Parent  6c177c4c212763c4f5ce8047e7f1eed22d9d06cd
Changed definitions so that qsplit is now defined in terms of
qfst, qsnd.  AT PRESENT THERE IS NO PATTERN-MATCHING FOR QSPLIT.

diff -r 6c177c4c2127 -r 01379c46ad2d src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Wed May 03 14:54:43 1995 +0200
+++ b/src/ZF/QPair.thy	Wed May 03 15:06:41 1995 +0200
@@ -14,8 +14,8 @@
 QPair = Sum + "simpdata" +
 consts
   QPair     :: "[i, i] => i"               	("<(_;/ _)>")
-  qsplit    :: "[[i,i] => i, i] => i"
-  qfsplit   :: "[[i,i] => o, i] => o"
+  qfst,qsnd :: "i => i"
+  qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
   qconverse :: "i => i"
   QSigma    :: "[i, i => i] => i"
 
@@ -33,8 +33,10 @@
 
 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)"
+  qfst_def        "qfst(p) == THE a. EX b. p=<a;b>"
+  qsnd_def        "qsnd(p) == THE b. EX a. p=<a;b>"
+  qsplit_def      "qsplit(c,p) == c(qfst(p), qsnd(p))"
+
   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>}"