[isabelle-dev] NEWS

[Fabian Immler]

* 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 
'print_atps'.

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.