--- 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: