NEWS
changeset 8736 0bfd6678a5fa
parent 8729 094dbd0fad0c
child 8788 518a5450ab6d
     1.1 --- a/NEWS	Tue Apr 18 14:57:18 2000 +0200
     1.2 +++ b/NEWS	Tue Apr 18 15:51:59 2000 +0200
     1.3 @@ -110,6 +110,9 @@
     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. in
     1.8 +   (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k;
     1.9 +
    1.10  * new version of "case_tac" subsumes both boolean case split and
    1.11  "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
    1.12  exists, may define val exhaust_tac = case_tac for ad-hoc portability;