equal
deleted
inserted
replaced
436 error "No ATP is set." |
436 error "No ATP is set." |
437 else case subgoal_count state of |
437 else case subgoal_count state of |
438 0 => (priority "No subgoal!"; (false, state)) |
438 0 => (priority "No subgoal!"; (false, state)) |
439 | n => |
439 | n => |
440 let |
440 let |
|
441 val _ = Proof.assert_backward state |
441 val thy = Proof.theory_of state |
442 val thy = Proof.theory_of state |
442 val timer = Timer.startRealTimer () |
443 val timer = Timer.startRealTimer () |
443 val _ = () |> not blocking ? kill_atps |
444 val _ = () |> not blocking ? kill_atps |
444 val _ = if auto then () else priority "Sledgehammering..." |
445 val _ = if auto then () else priority "Sledgehammering..." |
445 val provers = map (`(get_prover thy)) atps |
446 val provers = map (`(get_prover thy)) atps |