# HG changeset patch
# User lcp
# Date 794578728 -3600
# Node ID 137035296ad635e5f72007e682f8662d0a1f5fa5
# Parent  cb31a4e97f75c49453c86251393efcbea307d00d
Moved declarations of @QSUM and <*> to a syntax section.
Changed print_translation because <*> is now an infix.

diff -r cb31a4e97f75 -r 137035296ad6 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Tue Mar 07 13:15:25 1995 +0100
+++ b/src/ZF/QPair.thy	Tue Mar 07 13:18:48 1995 +0100
@@ -17,14 +17,16 @@
   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"
 
+syntax
+  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
+  "<*>"     :: "[i, i] => i"         		(infixr 80)
+
 translations
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
   "A <*> B"      => "QSigma(A, _K(B))"
@@ -45,4 +47,4 @@
 ML
 
 val print_translation =
-  [("QSigma", dependent_tr' ("@QSUM", "<*>"))];
+  [("QSigma", dependent_tr' ("@QSUM", "op <*>"))];