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

author | nipkow |

Mon, 04 Jan 1999 16:13:57 +0100 | |

changeset 6057 | 395ea7617554 |

parent 6056 | b21813d1b701 |

child 6058 | a9600c47ace3 |

*** empty log message ***

--- a/NEWS Mon Jan 04 15:08:40 1999 +0100 +++ b/NEWS Mon Jan 04 16:13:57 1999 +0100 @@ -1,4 +1,3 @@ - Isabelle NEWS -- history user-relevant changes ============================================== @@ -9,6 +8,13 @@ * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement +*** Proof tools *** + +* Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision +procedure for linear arithmetic. Currently it is used only for type `nat' in +HOL (see below) but can, should and will be instantiated for other types and +logics as well. + *** General *** * in locales, the "assumes" and "defines" parts may be omitted if empty; @@ -16,6 +22,17 @@ * new print_mode "xsymbols" for extended symbol support (e.g. genuiely long arrows) +*** HOL *** + +* There are now two decision procedures for linear arithmetic over nat: +1. nat_arith_tac copes with arbitrary propositional formulae (quantified +formulae are treated as atomic) involving `=', `<', `<=', 0, Suc, `+' and `-' +(other operators are treated as atomic). It has to be invoked by hand and is +a little bit slow. +2. fast_nat_arith_tac is a cut-down version of nat_arith_tac: it does not do +much propositional reasoning (hence the premises and the conclusion should be +as atomic as possible) and does not know about `-' either. It is fast and is +used automatically by the simplifier. *** Internal programming interfaces ***