*** empty log message ***
authornipkow
Fri May 17 11:36:32 2002 +0200 (2002-05-17)
changeset 131588e86582a90d1
parent 13157 4a4599f78f18
child 13159 2af7b94892ce
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Fri May 17 11:25:07 2002 +0200
     1.2 +++ b/NEWS	Fri May 17 11:36:32 2002 +0200
     1.3 @@ -1,7 +1,13 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 +*** HOL ***
     1.9 +
    1.10 +* arith(_tac) does now know about div 2 and mod 2 on type nat.
    1.11 +  It can solve simple goals like "0 < n ==> n div 2 < (n::nat)"
    1.12 +  but fails if divisibility plays a role like in
    1.13 +  "n div 2 + (n+1) div 2 = (n::nat)".
    1.14 +
    1.15  New in Isabelle2002 (March 2002)
    1.16  --------------------------------
    1.17