Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added parse rule for "<*>";
authorwenzelm
Fri, 08 Oct 1993 14:16:29 +0100
changeset 44 00597b21a6a9
parent 43 eb7ad4a7dc4f
child 45 48119aa914b2
added parse rule for "<*>"; removed ndependent_tr;
src/ZF/QPair.thy file | annotate | diff | comparison | revisions
src/ZF/qpair.thy file | annotate | diff | comparison | revisions 
--- 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", " <*>"))];
--- 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", " <*>"))];
isabelle