equal
deleted
inserted
replaced
531 |
531 |
532 val _ = |
532 val _ = |
533 Outer_Syntax.improper_command @{command_spec "quickcheck"} |
533 Outer_Syntax.improper_command @{command_spec "quickcheck"} |
534 "try to find counterexample for subgoal" |
534 "try to find counterexample for subgoal" |
535 (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => |
535 (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => |
536 Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i))); |
536 Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i))); |
537 |
537 |
538 |
538 |
539 (* automatic testing *) |
539 (* automatic testing *) |
540 |
540 |
541 fun try_quickcheck auto state = |
541 fun try_quickcheck auto state = |