src/Pure/Syntax/mixfix.ML
changeset 14855 a58abaad4f45
parent 14846 b1fcade3880b
child 14903 d264b8ad3eec
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Tue Jun 01 12:33:50 2004 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Tue Jun 01 12:35:46 2004 +0200
     1.3 @@ -266,10 +266,9 @@
     1.4    ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
     1.5    ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
     1.6    ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
     1.7 -  ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
     1.8 +  ("==",       "['a, 'a] => prop",      InfixrName ("\\<equiv>", 2)),
     1.9    ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    1.10    ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
    1.11 -  ("=?=",      "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>\\<^sup>?", 2)),
    1.12    ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
    1.13    ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    1.14    ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];