src/Pure/Syntax/mixfix.ML
changeset 2675 e2908f8edc8d
parent 2381 d00e6f44df79
child 2677 d73a46247a4a
equal deleted inserted replaced
2674:4385d521a691 2675:e2908f8edc8d
   193 val pure_sym_syntax =
   193 val pure_sym_syntax =
   194  [("fun",      "[type, type] => type",            Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   194  [("fun",      "[type, type] => type",            Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   195   ("_bracket", "[types, type] => type",           Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   195   ("_bracket", "[types, type] => type",           Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   196   ("_lambda",  "[idts, 'a] => logic",             Mixfix ("(3\\<lambda>_./ _)", [], 0)),
   196   ("_lambda",  "[idts, 'a] => logic",             Mixfix ("(3\\<lambda>_./ _)", [], 0)),
   197   ("==>",      "[prop, prop] => prop",            InfixrName ("\\<Midarrow>\\<Rightarrow>", 1)),
   197   ("==>",      "[prop, prop] => prop",            InfixrName ("\\<Midarrow>\\<Rightarrow>", 1)),
   198   ("_bigimpl", "[asms, prop] => prop",            Mixfix ("((3\\<lbrakk> _ \\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
   198   ("_bigimpl", "[asms, prop] => prop",            Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
   199   ("==",       "['a::{}, 'a] => prop",            InfixrName ("\\<equiv>", 2)),
   199   ("==",       "['a::{}, 'a] => prop",            InfixrName ("\\<equiv>", 2)),
   200   ("!!",       "[idts, prop] => prop",            Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
   200   ("!!",       "[idts, prop] => prop",            Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
   201 
   201 
   202 end;
   202 end;