Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Moved declarations of @QSUM and <*> to a syntax section.
authorlcp
Tue, 07 Mar 1995 13:18:48 +0100
changeset 929 137035296ad6
parent 928 cb31a4e97f75
child 930 63f02d32509e
Moved declarations of @QSUM and <*> to a syntax section. Changed print_translation because <*> is now an infix.
src/ZF/QPair.thy file | annotate | diff | comparison | revisions 
--- 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 <*>"))];
isabelle