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