--- 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;