immler at in.tum.de
Thu Oct 16 12:48:50 CEST 2008
* Generic ATP manager for Sledgehammer, based on ML threads instead of
Posix processes. Avoids potentially expensive forking of the ML process.
New thread-based implementation also works on non-Unix platforms
(Cygwin). Provers are no longer hardwired, but defined within the theory
via plain ML wrapper functions.
Basic sledgehammer commands:
- 'sledgehammer prover_1 ... prover_n' invokes the specified automated
theorem provers on the first subgoal. Provers are run in parallel, the
first successful result is displayed, and the other attempts are
terminated. Provers are defined in the theory context, see also
If no provers are given as arguments to sledgehammer, the system refers
to the default defined as "ATP provers" preference by the user
interface. There are additional preferences for timeout (default: 60
seconds), and the maximum number of independent prover processes
(default: 5); excessive provers are automatically terminated.
- 'print_atps' prints the list of automated theorem provers available to
the sledgehammer command.
- 'atp_info' prints information about presently running provers
- 'atp_kill' terminates all presently running provers.
More information about the isabelle-dev