# HG changeset patch
# User blanchet
# Date 1409179238 -7200
# Node ID f4d8987656b9c52e903af8c44d43b0b59c46c681
# Parent  3d060f43accb17a9ae59c928d0f11382102cb287
updated NEWS

diff -r 3d060f43accb -r f4d8987656b9 NEWS
--- a/NEWS	Thu Aug 28 00:40:38 2014 +0200
+++ b/NEWS	Thu Aug 28 00:40:38 2014 +0200
@@ -60,10 +60,15 @@
 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
 PARALLEL_GOALS.
 
-* Old SMT module:
-  - The 'smt' command has been renamed 'old_smt' and moved to
+* Old and new SMT modules:
+  - The old 'smt' command has been renamed 'old_smt' and moved to
     'src/HOL/Library/Old_SMT.thy'. It provided for compatibility, until
-    applications have been ported to use the new 'smt2' command.
+    applications have been ported to use the new 'smt2' command. For the
+    command to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must be
+    installed, and the environment variable "OLD_Z3_SOLVER" must point to
+    it.
+    INCOMPATIBILITY.
+  - The 'smt2' command has been renamed 'smt'.
     INCOMPATIBILITY.