--- a/src/Pure/Syntax/mixfix.ML Fri Apr 23 20:50:51 2004 +0200
+++ b/src/Pure/Syntax/mixfix.ML Fri Apr 23 20:52:04 2004 +0200
@@ -210,39 +210,40 @@
"asms", SynExt.any, SynExt.sprop, "num_const", "index", "struct"]);
val pure_syntax =
- [("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
- ("_abs", "'a", NoSyn),
- ("", "'a => " ^ SynExt.args, Delimfix "_"),
- ("_args", "['a, " ^ SynExt.args ^ "] => " ^ SynExt.args, Delimfix "_,/ _"),
- ("", "id => idt", Delimfix "_"),
- ("_idtyp", "[id, type] => idt", Mixfix ("_::_", [], 0)),
- ("", "idt => idt", Delimfix "'(_')"),
- ("", "idt => idts", Delimfix "_"),
- ("_idts", "[idt, idts] => idts", Mixfix ("_/ _", [1, 0], 0)),
- ("", "idt => pttrn", Delimfix "_"),
- ("", "pttrn => pttrns", Delimfix "_"),
- ("_pttrns", "[pttrn, pttrns] => pttrns", Mixfix ("_/ _", [1, 0], 0)),
- ("", "id => aprop", Delimfix "_"),
- ("", "longid => aprop", Delimfix "_"),
- ("", "var => aprop", Delimfix "_"),
- ("_DDDOT", "aprop", Delimfix "..."),
- ("_aprop", "aprop => prop", Delimfix "PROP _"),
- ("", "prop => asms", Delimfix "_"),
- ("_asms", "[prop, asms] => asms", Delimfix "_;/ _"),
- ("_bigimpl", "[asms, prop] => prop", Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
- ("_ofclass", "[type, logic] => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
- ("_mk_ofclass", "_", NoSyn),
- ("_TYPE", "type => logic", Delimfix "(1TYPE/(1'(_')))"),
- ("_K", "_", NoSyn),
- ("", "id => logic", Delimfix "_"),
- ("", "longid => logic", Delimfix "_"),
- ("", "var => logic", Delimfix "_"),
- ("_DDDOT", "logic", Delimfix "..."),
- ("_constify", "num => num_const", Delimfix "_"),
- ("_index", "num_const => index", Delimfix "\\<^sub>_"),
- ("_indexvar", "index", Delimfix "'\\<index>"),
- ("_noindex", "index", Delimfix ""),
- ("_struct", "index => logic", Delimfix "\\<struct>_")];
+ [("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
+ ("_abs", "'a", NoSyn),
+ ("", "'a => " ^ SynExt.args, Delimfix "_"),
+ ("_args", "['a, " ^ SynExt.args ^ "] => " ^ SynExt.args, Delimfix "_,/ _"),
+ ("", "id => idt", Delimfix "_"),
+ ("_idtyp", "[id, type] => idt", Mixfix ("_::_", [], 0)),
+ ("", "idt => idt", Delimfix "'(_')"),
+ ("", "idt => idts", Delimfix "_"),
+ ("_idts", "[idt, idts] => idts", Mixfix ("_/ _", [1, 0], 0)),
+ ("", "idt => pttrn", Delimfix "_"),
+ ("", "pttrn => pttrns", Delimfix "_"),
+ ("_pttrns", "[pttrn, pttrns] => pttrns", Mixfix ("_/ _", [1, 0], 0)),
+ ("", "id => aprop", Delimfix "_"),
+ ("", "longid => aprop", Delimfix "_"),
+ ("", "var => aprop", Delimfix "_"),
+ ("_DDDOT", "aprop", Delimfix "..."),
+ ("_aprop", "aprop => prop", Delimfix "PROP _"),
+ ("", "prop => asms", Delimfix "_"),
+ ("_asms", "[prop, asms] => asms", Delimfix "_;/ _"),
+ ("_bigimpl", "[asms, prop] => prop", Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
+ ("_ofclass", "[type, logic] => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
+ ("_mk_ofclass", "_", NoSyn),
+ ("_TYPE", "type => logic", Delimfix "(1TYPE/(1'(_')))"),
+ ("_K", "_", NoSyn),
+ ("", "id => logic", Delimfix "_"),
+ ("", "longid => logic", Delimfix "_"),
+ ("", "var => logic", Delimfix "_"),
+ ("_DDDOT", "logic", Delimfix "..."),
+ ("_constify", "num => num_const", Delimfix "_"),
+ ("_index", "num_const => index", Delimfix "\\<^sub>_"),
+ ("_indexlogic", "logic => index", Delimfix "\\<^bsub>_\\<^esub>"),
+ ("_indexvar", "index", Delimfix "'\\<index>"),
+ ("_noindex", "index", Delimfix ""),
+ ("_struct", "index => logic", Mixfix ("\\<struct>_", [1000], 1000))];
val pure_syntax_output =
[("Goal", "prop => prop", Mixfix ("_", [0], 0)),