changeset 13158 | 8e86582a90d1 |
parent 13042 | d8a345d9e067 |
child 13188 | 596776f878f8 |
--- 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) --------------------------------