# HG changeset patch
# User nipkow
# Date 1021628192 -7200
# Node ID 8e86582a90d115fbeeba70baddefa13935d37465
# Parent  4a4599f78f18020a60257bd1ac7feba2caf8f987
*** empty log message ***

diff -r 4a4599f78f18 -r 8e86582a90d1 NEWS
--- a/NEWS	Fri May 17 11:25:07 2002 +0200
+++ b/NEWS	Fri May 17 11:36:32 2002 +0200
@@ -1,7 +1,13 @@
-
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
+*** 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)"
+  but fails if divisibility plays a role like in
+  "n div 2 + (n+1) div 2 = (n::nat)".
+
 New in Isabelle2002 (March 2002)
 --------------------------------