# HG changeset patch
# User paulson
# Date 1253196286 -3600
# Node ID 1e2872252f913ef37281435a82cb2fdcf2128d50
# Parent  bd68c04dace1d9ce0cb118a7d301055173bf5cb2
NEWS: New method metisFT

diff -r bd68c04dace1 -r 1e2872252f91 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.: