# HG changeset patch
# User blanchet
# Date 1315818332 -7200
# Node ID 1c7991210f628f46587462a36345c8da67dbc9ec
# Parent  bdc64c34ccae42ae9b982ef2915b0d8a94848ba2
added my contributions to NEWS and CONTRIBUTORS

diff -r bdc64c34ccae -r 1c7991210f62 CONTRIBUTORS
--- 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
 -----------------------------
diff -r bdc64c34ccae -r 1c7991210f62 NEWS
--- 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: