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 1401 0c439768f45c
parent 1097 01379c46ad2d
child 1478 2b8c2a7547ab 
--- a/src/ZF/QPair.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/QPair.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -13,19 +13,19 @@
 
 QPair = Sum + "simpdata" +
 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