--- a/CONTRIBUTORS Mon Sep 12 10:49:37 2011 +0200
+++ b/CONTRIBUTORS Mon Sep 12 11:05:32 2011 +0200
@@ -16,6 +16,11 @@
Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
Prover IDE.
+* 2011: Jasmin Blanchette, TUM
+ Various improvements to Sledgehammer, notably: use of sound translations,
+ support for more provers (Waldmeister, LEO-II, Satallax). Further development
+ of Nitpick and "try".
+
Contributions to Isabelle2011
-----------------------------
--- a/NEWS Mon Sep 12 10:49:37 2011 +0200
+++ b/NEWS Mon Sep 12 11:05:32 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"
@@ -196,7 +199,7 @@
* Command 'try':
- Renamed 'try_methods' and added "simp:", "intro:", "dest:", and
"elim:" options. INCOMPATIBILITY.
- - Introduced 'tryÄ that not only runs 'try_methods' but also
+ - Introduced 'try' that not only runs 'try_methods' but also
'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.
* Quickcheck: