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