summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 6057 | 395ea7617554 |

parent 6028 | 1bfd52528bde |

child 6063 | aa2ac7d21792 |

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