equal
deleted
inserted
replaced
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 ((Binding.binding * Attrib.src list) * term) list -> (*{rules}*) |
8 local_theory -> local_theory |
8 local_theory -> local_theory |
|
9 |
9 val add_inductive: |
10 val add_inductive: |
10 (Binding.binding * string option * mixfix) list -> (*{predicates}*) |
11 (Binding.binding * string option * mixfix) list -> (*{predicates}*) |
11 (Binding.binding * string option * mixfix) list -> (*{parameters}*) |
12 (Binding.binding * string option * mixfix) list -> (*{parameters}*) |
12 (Attrib.binding * string) list -> (*{rules}*) |
13 (Attrib.binding * string) list -> (*{rules}*) |
13 local_theory -> local_theory |
14 local_theory -> local_theory |
168 in |
169 in |
169 add_inductive_i preds' params'' specs' lthy |
170 add_inductive_i preds' params'' specs' lthy |
170 end; |
171 end; |
171 (* @end *) |
172 (* @end *) |
172 |
173 |
173 (* @chunk syntax *) |
174 (* @chunk parser *) |
174 val parser = |
175 val parser = |
175 OuterParse.opt_target -- |
176 OuterParse.opt_target -- |
176 OuterParse.fixes -- |
177 OuterParse.fixes -- |
177 OuterParse.for_fixes -- |
178 OuterParse.for_fixes -- |
178 Scan.optional |
179 Scan.optional |
179 (OuterParse.$$$ "where" |-- |
180 (OuterParse.$$$ "where" |-- |
180 OuterParse.!!! |
181 OuterParse.!!! |
181 (OuterParse.enum1 "|" |
182 (OuterParse.enum1 "|" |
182 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) [] |
183 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) [] |
|
184 (* @end *) |
183 |
185 |
|
186 (* @chunk syntax *) |
184 val ind_decl = |
187 val ind_decl = |
185 parser >> |
188 parser >> |
186 (fn (((loc, preds), params), specs) => |
189 (fn (((loc, preds), params), specs) => |
187 Toplevel.local_theory loc (add_inductive preds params specs)) |
190 Toplevel.local_theory loc (add_inductive preds params specs)) |
188 |
191 |