NEWS

--- a/NEWS	Thu Sep 17 14:59:58 2009 +0100
+++ b/NEWS	Thu Sep 17 15:04:46 2009 +0100
@@ -127,6 +127,9 @@
 ATPs down considerably but eliminates a source of unsound "proofs"
 that fail later.
 
+* New method metisFT: A version of metis that uses full type information
+in order to avoid failures of proof reconstruction.
+
 * Discontinued ancient tradition to suffix certain ML module names
 with "_package", e.g.: