--- a/NEWS Mon Sep 12 12:33:37 2011 +0200
+++ b/NEWS Mon Sep 12 13:35:35 2011 +0200
@@ -180,10 +180,13 @@
INCOMPATIBILITY.
* Sledgehammer:
+ - Use quasi-sound (and efficient) translations by default.
+ - Added support for the following provers: E-ToFoF, LEO-II, Satallax, SNARK,
+ Waldmeister, and Z3 with TPTP syntax.
+ - Automatically preplay and minimize proofs before showing them if this can be
+ done within reasonable time.
- sledgehammer available_provers ~> sledgehammer supported_provers.
INCOMPATIBILITY.
- - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
- TPTP problems (TFF).
- Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters",
and "max_new_mono_instances" options.
- Removed "explicit_apply" and "full_types" options as well as "Full Types"