summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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