--- a/src/Pure/Syntax/mixfix.ML Sun Feb 11 16:34:20 2001 +0100
+++ b/src/Pure/Syntax/mixfix.ML Sun Feb 11 20:38:40 2001 +0100
@@ -224,6 +224,7 @@
val pure_xsym_syntax =
[("==>", "[prop, prop] => prop", InfixrName ("\\<Longrightarrow>", 1)),
+ ("=?=", "['a::{}, 'a] => prop", InfixrName ("\\<equiv>\\<^sup>?", 2)),
("_DDDOT", "aprop", Delimfix "\\<dots>"),
("_bigimpl", "[asms, prop] => prop", Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", "logic", Delimfix "\\<dots>")];