src/Pure/Syntax/mixfix.ML

   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
 
 val pure_xsym_syntax =
  [("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
-  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1))];
-
-end;
+  ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
+  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+  ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];
+
+end;