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; |