# HG changeset patch
# User wenzelm
# Date 1198153890 -3600
# Node ID 9728f319ffc67ea26d6325b44fbde777ad2e886b
# Parent  18bc59fb01b5c9af99695379d35216ffeb1d5d21
* Metis prover an order of magnitude faster, works with multithreading.

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;