# HG changeset patch
# User paulson
# Date 961156961 -7200
# Node ID 5ce73f3cadff3e2c076ff988c546df4a8a88614e
# Parent  090d450af656d73cd8a4004b8efce1fcb9fc30bb
real simprocs

diff -r 090d450af656 -r 5ce73f3cadff NEWS
--- a/NEWS	Fri Jun 16 13:41:44 2000 +0200
+++ b/NEWS	Fri Jun 16 14:02:41 2000 +0200
@@ -159,7 +159,7 @@
 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity.
 Types nat and int belong to this axclass;
 
-* greatly improved simplification involving numerals of type nat & int, e.g.
+* greatly improved simplification involving numerals of type nat, int, real:
    (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
    i*j + k + j*#3*i     simplifies to  #4*(i*j) + k
   two terms #m*u and #n*u are replaced by #(m+n)*u