# HG changeset patch
# User wenzelm
# Date 967572904 -7200
# Node ID 3a9f1931b30c4e013886b2eaac5372e9f16c1c32
# Parent  99fda46926ccad92409771313f3f3d2da5bc39c0
added \<dots> syntax;

diff -r 99fda46926cc -r 3a9f1931b30c src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Aug 29 20:14:42 2000 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Aug 29 20:15:04 2000 +0200
@@ -224,6 +224,8 @@
 
 val pure_xsym_syntax =
  [("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
-  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1))];
+  ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
+  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+  ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];
 
 end;