--- 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;