equal
deleted
inserted
replaced
525 |
525 |
526 val parse_args = |
526 val parse_args = |
527 @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed []; |
527 @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed []; |
528 |
528 |
529 val _ = |
529 val _ = |
530 Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing" |
530 Outer_Syntax.command @{command_keyword quickcheck_params} "set parameters for random testing" |
531 (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); |
531 (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); |
532 |
532 |
533 val _ = |
533 val _ = |
534 Outer_Syntax.command @{command_spec "quickcheck"} |
534 Outer_Syntax.command @{command_keyword quickcheck} |
535 "try to find counterexample for subgoal" |
535 "try to find counterexample for subgoal" |
536 (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => |
536 (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => |
537 Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i))); |
537 Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i))); |
538 |
538 |
539 |
539 |