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