src/Pure/Syntax/mixfix.ML
changeset 3027 ce99919010bf
parent 2767 e1d15eabb64d
child 3690 3f7053bf4237
equal deleted inserted replaced
3026:7a5611f66b72 3027:ce99919010bf
   157   map (fn t => (t, 0, NoSyn))
   157   map (fn t => (t, 0, NoSyn))
   158     (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
   158     (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
   159       "pttrn", "idt", "idts", "aprop", "asms", any, sprop, "dummy"]);
   159       "pttrn", "idt", "idts", "aprop", "asms", any, sprop, "dummy"]);
   160 
   160 
   161 val pure_syntax =
   161 val pure_syntax =
   162  [("_lambda",      "[idts, 'a] => logic",           Mixfix ("(3%_./ _)", [], 0)),
   162  [("_lambda",      "[idts, 'a] => logic",           Mixfix ("(3%_./ _)", [0, 3], 3)),
   163   ("_abs",         "'a",                            NoSyn),
   163   ("_abs",         "'a",                            NoSyn),
   164   ("",             "'a => " ^ args,                 Delimfix "_"),
   164   ("",             "'a => " ^ args,                 Delimfix "_"),
   165   ("_args",        "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"),
   165   ("_args",        "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"),
   166   ("",             "id => idt",                     Delimfix "_"),
   166   ("",             "id => idt",                     Delimfix "_"),
   167   ("_idtyp",       "[id, type] => idt",             Mixfix ("_::_", [], 0)),
   167   ("_idtyp",       "[id, type] => idt",             Mixfix ("_::_", [], 0)),
   196  [("fun",      "[type, type] => type",  Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   196  [("fun",      "[type, type] => type",  Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   197   ("_bracket", "[types, type] => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   197   ("_bracket", "[types, type] => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   198   ("_ofsort",  "[tid, sort] => type",   Mixfix ("_\\<Colon>_", [max_pri, 0], max_pri)),
   198   ("_ofsort",  "[tid, sort] => type",   Mixfix ("_\\<Colon>_", [max_pri, 0], max_pri)),
   199   ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
   199   ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
   200   ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
   200   ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
   201   ("_lambda",  "[idts, 'a] => logic",   Mixfix ("(3\\<lambda>_./ _)", [], 0)),
   201   ("_lambda",  "[idts, 'a] => logic",   Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
   202   ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Midarrow>\\<Rightarrow>", 1)),
   202   ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Midarrow>\\<Rightarrow>", 1)),
   203   ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
   203   ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
   204   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
   204   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
   205   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
   205   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
   206 
   206