# HG changeset patch
# User nipkow
# Date 1022824517 -7200
# Node ID 172f65d0c3d1fb2a9c8529f9000c3576d8c14c3a
# Parent  81ed5c6de8902e05f6dd7d38368947d757d92722
*** empty log message ***

diff -r 81ed5c6de890 -r 172f65d0c3d1 NEWS
--- a/NEWS	Fri May 31 07:53:37 2002 +0200
+++ b/NEWS	Fri May 31 07:55:17 2002 +0200
@@ -3,8 +3,8 @@
 
 *** HOL ***
 
-* arith(_tac) does now know about div 2 and mod 2 on type nat.
-  It can solve simple goals like "0 < n ==> n div 2 < (n::nat)"
+* arith(_tac) does now know about div k and mod k where k is a numeral of
+  type nat. 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: