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

NEWS

changeset 13881 | f63e2a057fd4 |

parent 13872 | 601514e63534 |

child 13899 | 12c7029d278b |

1.1 --- a/NEWS Tue Mar 25 09:50:53 2003 +0100 1.2 +++ b/NEWS Tue Mar 25 09:52:21 2003 +0100 1.3 @@ -131,6 +131,11 @@ 1.4 1.5 "n div 2 + (n+1) div 2 = (n::nat)" 1.6 1.7 +* New method / tactic presburger(_tac) for full Presburger arithmetic 1.8 + (by Amine Chaieb). Integrated with arith(_tac), i.e. presburger(_tac) 1.9 + is called automatically by arith(_tac), if the decision procedure for 1.10 + simple arithmetic fails to solve the goal. 1.11 + 1.12 * simp's arithmetic capabilities have been enhanced a bit: it now 1.13 takes ~= in premises into account (by performing a case split); 1.14