equal
deleted
inserted
replaced
101 val fold_thms: Proof.context -> thm list -> thm -> thm |
101 val fold_thms: Proof.context -> thm list -> thm -> thm |
102 |
102 |
103 val parse_type_args_named_constrained: (binding option * (string * string option)) list parser |
103 val parse_type_args_named_constrained: (binding option * (string * string option)) list parser |
104 val parse_map_rel_bindings: (binding * binding) parser |
104 val parse_map_rel_bindings: (binding * binding) parser |
105 |
105 |
106 val map_local_theory: (local_theory -> local_theory) -> theory -> theory |
|
107 val typedef: binding * (string * sort) list * mixfix -> term -> |
106 val typedef: binding * (string * sort) list * mixfix -> term -> |
108 (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory |
107 (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory |
109 end; |
108 end; |
110 |
109 |
111 structure BNF_Util : BNF_UTIL = |
110 structure BNF_Util : BNF_UTIL = |
138 |
137 |
139 val parse_map_rel_bindings = |
138 val parse_map_rel_bindings = |
140 @{keyword "for"} |-- Scan.repeat parse_map_rel_binding |
139 @{keyword "for"} |-- Scan.repeat parse_map_rel_binding |
141 >> (fn ps => fold extract_map_rel ps no_map_rel) |
140 >> (fn ps => fold extract_map_rel ps no_map_rel) |
142 || Scan.succeed no_map_rel; |
141 || Scan.succeed no_map_rel; |
143 |
|
144 fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global; |
|
145 |
142 |
146 fun typedef (b, Ts, mx) set opt_morphs tac lthy = |
143 fun typedef (b, Ts, mx) set opt_morphs tac lthy = |
147 let |
144 let |
148 (*Work around loss of qualification in "typedef" axioms by replicating it in the name*) |
145 (*Work around loss of qualification in "typedef" axioms by replicating it in the name*) |
149 val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b; |
146 val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b; |