# HG changeset patch
# User blanchet
# Date 1334781625 -7200
# Node ID 01f687b84affce552026e58bf493d2aef1d78657
# Parent  a72239723ae8d5799d9c9fab24b0864862f6fac9
Sledgehammer NEWS and CONTRIBUTORS

diff -r a72239723ae8 -r 01f687b84aff CONTRIBUTORS
--- 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.
diff -r a72239723ae8 -r 01f687b84aff NEWS
--- 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.