equal
deleted
inserted
replaced
2 signature SIMPLE_INDUCTIVE_PACKAGE = |
2 signature SIMPLE_INDUCTIVE_PACKAGE = |
3 sig |
3 sig |
4 val add_inductive_i: |
4 val add_inductive_i: |
5 ((Binding.binding * typ) * mixfix) list -> (*{predicates}*) |
5 ((Binding.binding * typ) * mixfix) list -> (*{predicates}*) |
6 (Binding.binding * typ) list -> (*{parameters}*) |
6 (Binding.binding * typ) list -> (*{parameters}*) |
7 ((Binding.binding * Attrib.src list) * term) list -> (*{rules}*) |
7 (Attrib.binding * term) list -> (*{rules}*) |
8 local_theory -> local_theory |
8 local_theory -> local_theory |
9 |
9 |
10 val add_inductive: |
10 val add_inductive: |
11 (Binding.binding * string option * mixfix) list -> (*{predicates}*) |
11 (Binding.binding * string option * mixfix) list -> (*{predicates}*) |
12 (Binding.binding * string option * mixfix) list -> (*{parameters}*) |
12 (Binding.binding * string option * mixfix) list -> (*{parameters}*) |