equal
deleted
inserted
replaced
626 fun initial_maps thy = |
626 fun initial_maps thy = |
627 thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool} |
627 thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool} |
628 |> add_hol4_type_mapping "min" "fun" false "fun" |
628 |> add_hol4_type_mapping "min" "fun" false "fun" |
629 |> add_hol4_type_mapping "min" "ind" false @{type_name ind} |
629 |> add_hol4_type_mapping "min" "ind" false @{type_name ind} |
630 |> add_hol4_const_mapping "min" "=" false @{const_name "op ="} |
630 |> add_hol4_const_mapping "min" "=" false @{const_name "op ="} |
631 |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"} |
631 |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies} |
632 |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"} |
632 |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"} |
633 in |
633 in |
634 val hol4_setup = |
634 val hol4_setup = |
635 initial_maps #> |
635 initial_maps #> |
636 Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule" |
636 Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule" |