# HG changeset patch
# User blanchet
# Date 1309179389 -7200
# Node ID 81f7dca3e5429f8aefbc956f1db3740ee19f2117
# Parent  ae612a423dad4728ff9d61ef029d6479dbd7e95a
minor Sledgehammer news

diff -r ae612a423dad -r 81f7dca3e542 NEWS
--- a/NEWS	Mon Jun 27 14:56:28 2011 +0200
+++ b/NEWS	Mon Jun 27 14:56:29 2011 +0200
@@ -85,12 +85,14 @@
     INCOMPATIBILITY.
   - 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.
+  - Added "type_sys", "sound", "max_mono_iters", and "max_new_mono_instances"
+    options.
   - Removed "full_types" option and corresponding Proof General menu item.
+    INCOMPATIBILITY.
 
 * Metis:
-  - Removed "metisF" -- use "metis" instead.
-  - Obsoleted "metisFT" -- use "metis (full_types)" instead.
+  - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
+  - Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY.
 
 * "try":
   - Renamed "try_methods" and added "simp:", "intro:", "dest:", and "elim:"