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