real simprocs
authorpaulson
Fri Jun 16 14:02:41 2000 +0200 (2000-06-16)
changeset 90855ce73f3cadff
parent 9084 090d450af656
child 9086 e4592e43e703
real simprocs
NEWS
     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