equal
deleted
inserted
replaced
8 *) |
8 *) |
9 |
9 |
10 signature BNF_GFP = |
10 signature BNF_GFP = |
11 sig |
11 sig |
12 val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list -> |
12 val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list -> |
13 binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list -> |
13 binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list -> |
14 local_theory -> BNF_FP.fp_result * local_theory |
14 local_theory -> BNF_FP.fp_result * local_theory |
15 end; |
15 end; |
16 |
16 |
17 structure BNF_GFP : BNF_GFP = |
17 structure BNF_GFP : BNF_GFP = |
18 struct |
18 struct |