# HG changeset patch
# User wenzelm
# Date 981920320 -3600
# Node ID a3299b153741fae409376076f6f7250eba49390f
# Parent  c1be9f2dff4ce1743b36869393de3f1214d2f918
added "xsymbols" syntax for "=?=";

diff -r c1be9f2dff4c -r a3299b153741 src/Pure/Syntax/mixfix.ML
--- 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>")];