NEWS
changeset 7157 d49318f6c11a
parent 7125 df7cf6e85501
child 7196 c8d1002060e8
     1.1 --- a/NEWS	Mon Aug 02 18:10:26 1999 +0200
     1.2 +++ b/NEWS	Tue Aug 03 13:04:50 1999 +0200
     1.3 @@ -107,6 +107,12 @@
     1.4  nat/int formulae where the two parts interact, such as `m < n ==>
     1.5  int(m) < int(n)'.
     1.6  
     1.7 +* An interface to the Stanford Validity Checker (SVC) is available through 
     1.8 +  the tactic svc_tac.  Propositional tautologies and theorems of linear
     1.9 +  arithmetic are proved automatically.  Numeric variables may have types nat, 
    1.10 +  int or real.  SVC must be installed separately, and 
    1.11 +  its results must be TAKEN ON TRUST (Isabelle does not check the proofs).
    1.12 +
    1.13  * Integer division and remainder can now be performed on constant arguments.  
    1.14  
    1.15  * Many properties of integer multiplication, division and remainder are now