# HG changeset patch
# User wenzelm
# Date 1275508383 -7200
# Node ID 1f3ca94ccb84425fd3cb716b05d13987d8339877
# Parent  a1acd424645a73918075bb1d3887a4b411529d7b
improved parallelism of proof term normalization;

diff -r a1acd424645a -r 1f3ca94ccb84 NEWS
--- a/NEWS	Wed Jun 02 21:39:35 2010 +0200
+++ b/NEWS	Wed Jun 02 21:53:03 2010 +0200
@@ -86,6 +86,9 @@
 'hide_fact' replace the former 'hide' KIND command.  Minor
 INCOMPATIBILITY.
 
+* Improved parallelism of proof term normalization: usedir -p2 -q0 is
+more efficient than combinations with -q1 or -q2.
+
 
 *** Pure ***