611 else F (Name.variant used pdefname) (* last resort *) |
611 else F (Name.variant used pdefname) (* last resort *) |
612 end |
612 end |
613 end |
613 end |
614 |
614 |
615 local |
615 local |
616 fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x |
616 fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x |
617 | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x |
617 | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x |
618 | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x |
618 | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x |
619 | handle_meta [x] = Appl[Constant "Trueprop",x] |
619 | handle_meta [x] = Appl[Constant "Trueprop",x] |
620 | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument" |
620 | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument" |
621 in |
621 in |
622 val smarter_trueprop_parsing = [("Trueprop",handle_meta)] |
622 val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)] |
623 end |
623 end |
624 |
624 |
625 local |
625 local |
626 fun initial_maps thy = |
626 fun initial_maps thy = |
627 thy |> add_hol4_type_mapping "min" "bool" false "bool" |
627 thy |> add_hol4_type_mapping "min" "bool" false "bool" |