src/Pure/Syntax/mixfix.ML
changeset 11098 a3299b153741
parent 9734 3a9f1931b30c
child 11651 201b3f76c7b7
equal deleted inserted replaced
11097:c1be9f2dff4c 11098:a3299b153741
   222   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
   222   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
   223   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
   223   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
   224 
   224 
   225 val pure_xsym_syntax =
   225 val pure_xsym_syntax =
   226  [("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
   226  [("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
       
   227   ("=?=",      "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>\\<^sup>?", 2)),
   227   ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
   228   ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
   228   ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   229   ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   229   ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];
   230   ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];
   230 
   231 
   231 end;
   232 end;