(* ------------------------------------------------------------------------- *) (* Some additional infixes to support Freek's "Mizar Light". *) (* ------------------------------------------------------------------------- *) open Pcaml; Pcaml.syntax_name.val := "Freek"; Format.print_string "New infixes set up"; Format.print_newline(); EXTEND expr: AFTER "<" [[ f = expr; "by"; g = expr -> <:expr< ((by $f$) $g$) >> | f = expr; "st'"; g = expr -> <:expr< ((st' $f$) $g$) >> | f = expr; "st"; g = expr -> <:expr< ((st $f$) $g$) >> | f = expr; "at"; g = expr -> <:expr< ((at $f$) $g$) >> | f = expr; "from"; g = expr -> <:expr< ((from $f$) $g$) >> | f = expr; "using"; g = expr -> <:expr< ((using $f$) $g$) >> | f = expr; "proof"; g = expr -> <:expr< ((proof $f$) $g$) >> | f = expr; "THEN'"; g = expr -> <:expr< ((then'_ $f$) $g$) >> ]]; END;