NEWS
changeset 8788 518a5450ab6d
parent 8736 0bfd6678a5fa
child 8832 bcceda950cd0
     1.1 --- a/NEWS	Thu May 04 12:29:00 2000 +0200
     1.2 +++ b/NEWS	Thu May 04 12:29:18 2000 +0200
     1.3 @@ -7,6 +7,11 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES (see below for more details) ***
     1.6  
     1.7 +* HOL: simplification of natural numbers is much changed.  To partly recover
     1.8 +       the old behaviour (e.g. to prevent n+n rewriting to #2*n) type
     1.9 +		Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
    1.10 +		Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
    1.11 +
    1.12  * HOL: the constant for f``x is now "image" rather than "op ``";
    1.13  
    1.14  * HOL: the cartesian product is now "<*>" instead of "Times"; the
    1.15 @@ -110,8 +115,9 @@
    1.16  basically a generalized version of de-Bruijn representation; very
    1.17  useful in avoiding lifting all operations;
    1.18  
    1.19 -* greatly improved simplification involving numerals of type "nat", e.g. in
    1.20 -   (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k;
    1.21 +* greatly improved simplification involving numerals of type "nat", e.g.
    1.22 +   (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
    1.23 +   i*j + k + j*#3*i     simplifies to  #4*(i*j) + k;
    1.24  
    1.25  * new version of "case_tac" subsumes both boolean case split and
    1.26  "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer