Update from HH
[hl193./.git] / Mizarlight / pa_f.ml
1 (* ------------------------------------------------------------------------- *)
2 (* Some additional infixes to support Freek's "Mizar Light".                 *)
3 (* ------------------------------------------------------------------------- *)
4
5 open Pcaml;
6
7 Pcaml.syntax_name.val := "Freek";
8
9 Format.print_string "New infixes set up";
10 Format.print_newline();
11
12 EXTEND
13   expr: AFTER "<"
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$) >>
22
23    ]];
24
25 END;