diff -r 18bc59fb01b5 -r 9728f319ffc6 NEWS
--- a/NEWS	Thu Dec 20 12:02:46 2007 +0100
+++ b/NEWS	Thu Dec 20 13:31:30 2007 +0100
@@ -51,10 +51,13 @@
 for examples,
 
 * Records. Removed K_record, and replaced it by pure lambda term
-%x. c. The simplifier setup is now more robust against eta
-expansion. 
+%x. c. The simplifier setup is now more robust against eta expansion.
 INCOMPATIBILITY: in cases explicitly referring to K_record.
 
+* Metis prover is now an order of magnitude faster, and also works
+with multithreading.
+
+
 *** System ***
 
 * isatool tty runs Isabelle process with plain tty interaction;