7 *) |
7 *) |
8 |
8 |
9 signature BNF_LFP = |
9 signature BNF_LFP = |
10 sig |
10 sig |
11 val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> |
11 val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> |
12 typ list * typ list list -> BNF_Def.BNF list -> local_theory -> |
12 typ list * typ list list -> BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory |
13 (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list * |
|
14 thm list * thm list * thm list * thm list list * thm list * thm list * thm list) * |
|
15 local_theory |
|
16 end; |
13 end; |
17 |
14 |
18 structure BNF_LFP : BNF_LFP = |
15 structure BNF_LFP : BNF_LFP = |
19 struct |
16 struct |
20 |
17 |
1829 |> maps (fn (thmN, thmss) => |
1826 |> maps (fn (thmN, thmss) => |
1830 map2 (fn b => fn thms => |
1827 map2 (fn b => fn thms => |
1831 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
1828 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
1832 bs thmss) |
1829 bs thmss) |
1833 in |
1830 in |
1834 ((Ibnfs, dtors, ctors, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, |
1831 ((Ibnfs, dtors, ctors, folds, recs, ctor_induct_thm, ctor_induct_thm, dtor_ctor_thms, |
1835 ctor_inject_thms, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, |
1832 ctor_dtor_thms, ctor_inject_thms, folded_ctor_map_thms, folded_ctor_set_thmss', |
1836 ctor_fold_thms, ctor_rec_thms), |
1833 ctor_Irel_thms, ctor_fold_thms, ctor_rec_thms), |
1837 lthy |> Local_Theory.notes (common_notes @ notes) |> snd) |
1834 lthy |> Local_Theory.notes (common_notes @ notes) |> snd) |
1838 end; |
1835 end; |
1839 |
1836 |
1840 val _ = |
1837 val _ = |
1841 Outer_Syntax.local_theory @{command_spec "data_raw"} |
1838 Outer_Syntax.local_theory @{command_spec "data_raw"} |