--- a/CONTRIBUTORS Wed Apr 18 22:40:25 2012 +0200
+++ b/CONTRIBUTORS Wed Apr 18 22:40:25 2012 +0200
@@ -17,9 +17,13 @@
Alexander Krauss, QAware GmbH
Faster and more scalable Import mechanism for HOL Light proofs.
-* January 2012: Florian Haftmann, TUM, et. al.
+* January 2012: Florian Haftmann, TUM, et al.
(Re-)Introduction of the "set" type constructor.
+* 2011/2012: Jasmin Blanchette, TUM
+ Various improvements to Sledgehammer, notably: tighter integration
+ with SPASS, support for more provers (Alt-Ergo, iProver, iProver-Eq).
+
* 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
Various refinements of local theory infrastructure.
Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.
--- a/NEWS Wed Apr 18 22:40:25 2012 +0200
+++ b/NEWS Wed Apr 18 22:40:25 2012 +0200
@@ -617,11 +617,17 @@
conjectures in a locale context.
* Nitpick:
-
- Fixed infinite loop caused by the 'peephole_optim' option and
affecting 'rat' and 'real'.
* Sledgehammer:
+ - Integrated more tightly with SPASS, as described in the ITP 2012 paper "More
+ SPASS with Isabelle".
+ - Made it try "smt" as a fallback if "metis" fails or times out.
+ - Added support for the following provers: Alt-Ergo (via Why3 and TFF1),
+ iProver, iProver-Eq.
+ - Replaced remote E-SInE with remote Satallax in the default setup.
+ - Sped up the minimizer.
- Added "lam_trans", "uncurry_aliases", and "minimize" options.
- Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
- Renamed "sound" option to "strict".
@@ -631,7 +637,7 @@
parenthesized argument (e.g., "by (metis (lifting) ...)").
* SMT:
- - renamed "smt_fixed" option to "smt_read_only_certificates".
+ - Renamed "smt_fixed" option to "smt_read_only_certificates".
* Command 'try0':
- Renamed from 'try_methods'. INCOMPATIBILITY.