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 bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> Proof.context -> |
11 val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory -> |
12 (term list * term list * thm list * thm list) * Proof.context |
12 (term list * term list * thm list * thm list) * local_theory |
13 end; |
13 end; |
14 |
14 |
15 structure BNF_LFP : BNF_LFP = |
15 structure BNF_LFP : BNF_LFP = |
16 struct |
16 struct |
17 |
17 |