src/ZF/QPair.thy

   QInl,QInr :: "i=>i"
   qcase     :: "[i=>i, i=>i, i]=>i"
 
 translations
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
+  "A <*> B"      => "QSigma(A, _K(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)"

   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", " <*>"))];