--- a/src/ZF/QPair.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/QPair.thy Thu Apr 26 14:24:08 2007 +0200
@@ -41,12 +41,13 @@
"QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
syntax
- "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
- "<*>" :: "[i, i] => i" (infixr 80)
-
+ "_QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
translations
"QSUM x:A. B" => "QSigma(A, %x. B)"
- "A <*> B" => "QSigma(A, %_. B)"
+
+abbreviation
+ qprod (infixr "<*>" 80) where
+ "A <*> B == QSigma(A, %_. B)"
constdefs
qsum :: "[i,i]=>i" (infixr "<+>" 65)
@@ -62,9 +63,6 @@
"qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))"
-print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
-
-
subsection{*Quine ordered pairing*}
(** Lemmas for showing that <a;b> uniquely determines a and b **)
@@ -386,4 +384,3 @@
*}
end
-