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 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2469 b50b8c0eec01 
--- a/src/ZF/QPair.thy	Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/QPair.thy	Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/qpair.thy
+(*  Title:      ZF/qpair.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
@@ -13,19 +13,19 @@
 
 QPair = Sum + "simpdata" +
 consts
-  QPair     :: [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)
+  "<+>"     :: [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)
+  "<*>"     :: [i, i] => i                      (infixr 80)
 
 translations
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
isabelle