equal
deleted
inserted
replaced
1 (* @chunk SIMPLE_INDUCTIVE_PACKAGE *) |
1 (* @chunk SIMPLE_INDUCTIVE_PACKAGE *) |
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.T * typ) * mixfix) list -> (*{predicates}*) |
5 ((Binding.binding * typ) * mixfix) list -> (*{predicates}*) |
6 (Binding.T * typ) list -> (*{parameters}*) |
6 (Binding.binding * typ) list -> (*{parameters}*) |
7 (Attrib.binding * term) list -> (*{rules}*) |
7 (Attrib.binding * term) list -> (*{rules}*) |
8 local_theory -> (thm list * thm list) * local_theory |
8 local_theory -> (thm list * thm list) * local_theory |
9 val add_inductive: |
9 val add_inductive: |
10 (Binding.T * string option * mixfix) list -> (*{predicates}*) |
10 (Binding.binding * string option * mixfix) list -> (*{predicates}*) |
11 (Binding.T * string option * mixfix) list -> (*{parameters}*) |
11 (Binding.binding * string option * mixfix) list -> (*{parameters}*) |
12 (Attrib.binding * string) list -> (*{rules}*) |
12 (Attrib.binding * string) list -> (*{rules}*) |
13 local_theory -> (thm list * thm list) * local_theory |
13 local_theory -> (thm list * thm list) * local_theory |
14 end; |
14 end; |
15 (* @end *) |
15 (* @end *) |
16 |
16 |