1 (* ------------------------------------------------------------------------- *)
2 (* Some additional infixes to support Freek's "Mizar Light". *)
3 (* ------------------------------------------------------------------------- *)
7 Pcaml.syntax_name.val := "Freek";
9 Format.print_string "New infixes set up";
10 Format.print_newline();
14 [[ f = expr; "by"; g = expr -> <:expr< ((by $f$) $g$) >>
15 | f = expr; "st'"; g = expr -> <:expr< ((st' $f$) $g$) >>
16 | f = expr; "st"; g = expr -> <:expr< ((st $f$) $g$) >>
17 | f = expr; "at"; g = expr -> <:expr< ((at $f$) $g$) >>
18 | f = expr; "from"; g = expr -> <:expr< ((from $f$) $g$) >>
19 | f = expr; "using"; g = expr -> <:expr< ((using $f$) $g$) >>
20 | f = expr; "proof"; g = expr -> <:expr< ((proof $f$) $g$) >>
21 | f = expr; "THEN'"; g = expr -> <:expr< ((then'_ $f$) $g$) >>