changeset 6093 | 87bf8c03b169 |
parent 3940 | 1d5bee4d047f |
child 13220 | 62c899c77151 |
--- a/src/ZF/QPair.thy Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/QPair.thy Tue Jan 12 15:17:37 1999 +0100 @@ -13,8 +13,6 @@ QPair = Sum + -global - consts QPair :: [i, i] => i ("<(_;/ _)>") qfst,qsnd :: i => i @@ -34,7 +32,6 @@ "QSUM x:A. B" => "QSigma(A, %x. B)" "A <*> B" => "QSigma(A, _K(B))" -local defs QPair_def "<a;b> == a+b"