changeset 44 | 00597b21a6a9 |
parent 0 | a5a9c433f639 |
child 120 | 09287f26bfb8 |
--- a/src/ZF/QPair.thy Fri Oct 08 14:11:12 1993 +0100 +++ b/src/ZF/QPair.thy Fri Oct 08 14:16:29 1993 +0100 @@ -27,6 +27,7 @@ translations "QSUM x:A. B" => "QSigma(A, %x. B)" + "A <*> B" => "QSigma(A, _K(B))" rules QPair_def "<a;b> == a+b" @@ -43,10 +44,5 @@ ML -(* 'Dependent' type operators *) - -val parse_translation = - [(" <*>", ndependent_tr "QSigma")]; - val print_translation = [("QSigma", dependent_tr' ("@QSUM", " <*>"))];