NEWS
changeset 43570 ccfb3623a68a
parent 43527 1aacef7471c2
child 43573 81f7dca3e542
--- 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