# HG changeset patch
# User blanchet
# Date 1309179370 -7200
# Node ID ccfb3623a68a90a9a779015fdfe2b62144115462
# Parent  b342cd12553343739edf4055375397c3f24ad29c
document changes to Sledgehammer and "try"

diff -r b342cd125533 -r ccfb3623a68a NEWS
--- a/NEWS	Mon Jun 27 13:52:47 2011 +0200
+++ b/NEWS	Mon Jun 27 14:56:10 2011 +0200
@@ -86,13 +86,17 @@
   - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
     TPTP problems (TFF).
   - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
+  - Removed "full_types" option and corresponding Proof General menu item.
 
 * Metis:
   - Removed "metisF" -- use "metis" instead.
   - Obsoleted "metisFT" -- use "metis (full_types)" instead.
 
 * "try":
-  - Added "simp:", "intro:", and "elim:" options.
+  - Renamed "try_methods" and added "simp:", "intro:", "dest:", and "elim:"
+    options. INCOMPATIBILITY.
+  - Introduced "try" that not only runs "try_methods" but also "solve_direct",
+    "sledgehammer", "quickcheck", and "nitpick".
 
 * Quickcheck:
   - Added "eval" option to evaluate terms for the found counterexample