# HG changeset patch
# User nipkow
# Date 1022746888 -7200
# Node ID 596776f878f83f10b1f42a96cdfbf55ed667a20c
# Parent  e5434b822a961088ebaddf6ea17a8d40b0de0de6
*** empty log message ***

diff -r e5434b822a96 -r 596776f878f8 NEWS
--- a/NEWS	Thu May 30 10:12:52 2002 +0200
+++ b/NEWS	Thu May 30 10:21:28 2002 +0200
@@ -7,6 +7,8 @@
   It can solve simple goals like "0 < n ==> n div 2 < (n::nat)"
   but fails if divisibility plays a role like in
   "n div 2 + (n+1) div 2 = (n::nat)".
+* simp's arithmetic capabilities have been enhanced a bit:
+  it now takes ~= in premises into account (by performing a case split).
 
 New in Isabelle2002 (March 2002)
 --------------------------------