equal
deleted
inserted
replaced
6 Datatype construction. |
6 Datatype construction. |
7 *) |
7 *) |
8 |
8 |
9 signature BNF_LFP = |
9 signature BNF_LFP = |
10 sig |
10 sig |
11 val construct_lfp: mixfix list -> binding list -> binding list -> binding list -> |
11 val construct_lfp: mixfix list -> binding list -> binding list -> binding list list -> |
12 binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> |
12 binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> |
13 local_theory -> BNF_FP_Util.fp_result * local_theory |
13 local_theory -> BNF_FP_Util.fp_result * local_theory |
14 end; |
14 end; |
15 |
15 |
16 structure BNF_LFP : BNF_LFP = |
16 structure BNF_LFP : BNF_LFP = |
17 struct |
17 struct |
24 open BNF_FP_Def_Sugar |
24 open BNF_FP_Def_Sugar |
25 open BNF_LFP_Util |
25 open BNF_LFP_Util |
26 open BNF_LFP_Tactics |
26 open BNF_LFP_Tactics |
27 |
27 |
28 (*all BNFs have the same lives*) |
28 (*all BNFs have the same lives*) |
29 fun construct_lfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy = |
29 fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy = |
30 let |
30 let |
31 val timer = time (Timer.startRealTimer ()); |
31 val timer = time (Timer.startRealTimer ()); |
32 |
32 |
33 val note_all = Config.get lthy bnf_note_all; |
33 val note_all = Config.get lthy bnf_note_all; |
34 |
34 |