equal
deleted
inserted
replaced
647 |> add_hol4_const_mapping "min" "==>" false "op -->" |
647 |> add_hol4_const_mapping "min" "==>" false "op -->" |
648 |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps" |
648 |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps" |
649 in |
649 in |
650 val hol4_setup = |
650 val hol4_setup = |
651 initial_maps #> |
651 initial_maps #> |
652 Attrib.add_attributes |
652 Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule" |
653 [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")] |
653 |
654 end |
654 end |