# HG changeset patch
# User wenzelm
# Date 750086189 -3600
# Node ID 00597b21a6a963eac7acf3054af0171a6d7dedb9
# Parent  eb7ad4a7dc4fe0cf8a5aec708c1f7d44c91ee088
added parse rule for "<*>";
removed ndependent_tr;

diff -r eb7ad4a7dc4f -r 00597b21a6a9 src/ZF/QPair.thy
--- 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", " <*>"))];
diff -r eb7ad4a7dc4f -r 00597b21a6a9 src/ZF/qpair.thy
--- 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", " <*>"))];