summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 03 Aug 1999 13:04:50 +0200 | |

changeset 7157 | d49318f6c11a |

parent 7156 | 3e84e73a3b6a |

child 7158 | ac93579530ea |

SVC

--- 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