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

NEWS

changeset 9085 | 5ce73f3cadff |

parent 9057 | af1ca1acf292 |

child 9185 | 30d46270a427 |

1.1 --- a/NEWS Fri Jun 16 13:41:44 2000 +0200 1.2 +++ b/NEWS Fri Jun 16 14:02:41 2000 +0200 1.3 @@ -159,7 +159,7 @@ 1.4 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity. 1.5 Types nat and int belong to this axclass; 1.6 1.7 -* greatly improved simplification involving numerals of type nat & int, e.g. 1.8 +* greatly improved simplification involving numerals of type nat, int, real: 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 two terms #m*u and #n*u are replaced by #(m+n)*u