equal
deleted
inserted
replaced
276 |
276 |
277 |
277 |
278 (* code_pred command and values command *) |
278 (* code_pred command and values command *) |
279 |
279 |
280 val _ = |
280 val _ = |
281 Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"} |
281 Outer_Syntax.local_theory_to_proof @{command_keyword code_pred} |
282 "prove equations for predicate specified by intro/elim rules" |
282 "prove equations for predicate specified by intro/elim rules" |
283 (opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd) |
283 (opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd) |
284 |
284 |
285 val _ = |
285 val _ = |
286 Outer_Syntax.command @{command_spec "values"} |
286 Outer_Syntax.command @{command_keyword values} |
287 "enumerate and print comprehensions" |
287 "enumerate and print comprehensions" |
288 (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term |
288 (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term |
289 >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep |
289 >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep |
290 (Predicate_Compile_Core.values_cmd print_modes param_modes options k t))) |
290 (Predicate_Compile_Core.values_cmd print_modes param_modes options k t))) |
291 |
291 |