"..." syntax;
authorwenzelm
Wed, 02 Jun 1999 22:25:57 +0200
changeset 6759 8ce58492bf50
parent 6758 8fc15183f549
child 6760 1c56eb841afe
"..." syntax;
src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Jun 02 11:55:18 1999 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Jun 02 22:25:57 1999 +0200
@@ -197,7 +197,8 @@
   ("",             "id => logic",                   Delimfix "_"),
   ("",             "longid => logic",               Delimfix "_"),
   ("",             "var => logic",                  Delimfix "_"),
-  ("_BIND",        "id => logic",                   Delimfix "??_")];
+  ("_BIND",        "id => logic",                   Delimfix "??_"),
+  ("_DDDOT",       "logic",                         Delimfix "...")];
 
 val pure_appl_syntax =
  [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),