# HG changeset patch
# User paulson
# Date 933678290 -7200
# Node ID d49318f6c11ad8e57ebdf2192f466bcc039e2a4a
# Parent  3e84e73a3b6a7382df87dcfbd9f7d1bd0cb8a4e0
SVC

diff -r 3e84e73a3b6a -r d49318f6c11a NEWS
--- a/NEWS	Mon Aug 02 18:10:26 1999 +0200
+++ b/NEWS	Tue Aug 03 13:04:50 1999 +0200
@@ -107,6 +107,12 @@
 nat/int formulae where the two parts interact, such as `m < n ==>
 int(m) < int(n)'.
 
+* An interface to the Stanford Validity Checker (SVC) is available through 
+  the tactic svc_tac.  Propositional tautologies and theorems of linear
+  arithmetic are proved automatically.  Numeric variables may have types nat, 
+  int or real.  SVC must be installed separately, and 
+  its results must be TAKEN ON TRUST (Isabelle does not check the proofs).
+
 * Integer division and remainder can now be performed on constant arguments.  
 
 * Many properties of integer multiplication, division and remainder are now