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

NEWS

changeset 8832 | bcceda950cd0 |

parent 8788 | 518a5450ab6d |

child 8848 | b06d183df34d |

1.1 --- a/NEWS Mon May 08 11:45:57 2000 +0200 1.2 +++ b/NEWS Mon May 08 16:57:53 2000 +0200 1.3 @@ -115,9 +115,13 @@ 1.4 basically a generalized version of de-Bruijn representation; very 1.5 useful in avoiding lifting all operations; 1.6 1.7 -* greatly improved simplification involving numerals of type "nat", e.g. 1.8 +* greatly improved simplification involving numerals of type nat & int, e.g. 1.9 (i + #8 + j) = Suc k simplifies to #7 + (i + j) = k 1.10 - i*j + k + j*#3*i simplifies to #4*(i*j) + k; 1.11 + i*j + k + j*#3*i simplifies to #4*(i*j) + k 1.12 + two terms #m*u and #n*u are replaced by #(m+n)*u 1.13 + (where #m, #n and u can implicitly be 1; this is simproc combine_numerals) 1.14 + and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y 1.15 + or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals); 1.16 1.17 * new version of "case_tac" subsumes both boolean case split and 1.18 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer