equal
deleted
inserted
replaced
5 Wrapping existing datatypes. |
5 Wrapping existing datatypes. |
6 *) |
6 *) |
7 |
7 |
8 signature BNF_WRAP = |
8 signature BNF_WRAP = |
9 sig |
9 sig |
|
10 val wrap: ({prems: thm list, context: Proof.context} -> tactic) list list -> |
|
11 (term list * term) * (binding list * binding list list) -> Proof.context -> local_theory |
10 end; |
12 end; |
11 |
13 |
12 structure BNF_Wrap : BNF_WRAP = |
14 structure BNF_Wrap : BNF_WRAP = |
13 struct |
15 struct |
14 |
16 |
403 end; |
405 end; |
404 in |
406 in |
405 (goals, after_qed, lthy') |
407 (goals, after_qed, lthy') |
406 end; |
408 end; |
407 |
409 |
|
410 fun wrap tacss = (fn (goalss, after_qed, lthy) => |
|
411 map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss |
|
412 |> (fn thms => after_qed thms lthy)) oo |
|
413 prepare_wrap (singleton o Type_Infer_Context.infer_types) |
|
414 |
408 val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; |
415 val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; |
409 |
416 |
410 val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; |
417 val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; |
411 |
418 |
412 val wrap_data_cmd = (fn (goalss, after_qed, lthy) => |
419 val wrap_data_cmd = (fn (goalss, after_qed, lthy) => |