src/ZF/QPair.thy
changeset 6093 87bf8c03b169
parent 3940 1d5bee4d047f
child 13220 62c899c77151
     1.1 --- a/src/ZF/QPair.thy	Tue Jan 12 13:54:51 1999 +0100
     1.2 +++ b/src/ZF/QPair.thy	Tue Jan 12 15:17:37 1999 +0100
     1.3 @@ -13,8 +13,6 @@
     1.4  
     1.5  QPair = Sum +
     1.6  
     1.7 -global
     1.8 -
     1.9  consts
    1.10    QPair     :: [i, i] => i                      ("<(_;/ _)>")
    1.11    qfst,qsnd :: i => i
    1.12 @@ -34,7 +32,6 @@
    1.13    "QSUM x:A. B"  => "QSigma(A, %x. B)"
    1.14    "A <*> B"      => "QSigma(A, _K(B))"
    1.15  
    1.16 -local
    1.17  
    1.18  defs
    1.19    QPair_def       "<a;b> == a+b"