268 ((NONE, false), (Pred, [])) |
268 ((NONE, false), (Pred, [])) |
269 end |
269 end |
270 |
270 |
271 (* code_pred command and values command *) |
271 (* code_pred command and values command *) |
272 |
272 |
273 val _ = Outer_Syntax.local_theory_to_proof "code_pred" |
273 val _ = |
274 "prove equations for predicate specified by intro/elim rules" |
274 Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"} |
275 Keyword.thy_goal |
275 "prove equations for predicate specified by intro/elim rules" |
276 (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd) |
276 (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd) |
277 |
277 |
278 val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag |
278 val _ = |
279 (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term |
279 Outer_Syntax.improper_command @{command_spec "values"} |
280 >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep |
280 "enumerate and print comprehensions" |
281 (Predicate_Compile_Core.values_cmd print_modes param_modes options k t))); |
281 (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term |
|
282 >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep |
|
283 (Predicate_Compile_Core.values_cmd print_modes param_modes options k t))) |
282 |
284 |
283 end |
285 end |