Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/QPair.thy
changeset 13220 62c899c77151
parent 6093 87bf8c03b169
child 13259 01fa0c8dbc92 
--- a/src/ZF/QPair.thy	Tue Jun 18 17:58:21 2002 +0200
+++ b/src/ZF/QPair.thy	Tue Jun 18 18:45:07 2002 +0200
@@ -14,19 +14,19 @@
 QPair = Sum +
 
 consts
-  QPair     :: [i, i] => i                      ("<(_;/ _)>")
-  qfst,qsnd :: i => i
-  qsplit    :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
-  qconverse :: i => i
-  QSigma    :: [i, i => i] => i
+  QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
+  qfst,qsnd :: "i => i"
+  qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
+  qconverse :: "i => i"
+  QSigma    :: "[i, i => i] => i"
 
-  "<+>"     :: [i,i]=>i                         (infixr 65)
-  QInl,QInr :: i=>i
-  qcase     :: [i=>i, 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)
+  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
+  "<*>"     :: "[i, i] => i"                      (infixr 80)
 
 translations
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
isabelle