*** empty log message ***
authornipkow
Fri May 31 07:55:17 2002 +0200 (2002-05-31)
changeset 13190172f65d0c3d1
parent 13189 81ed5c6de890
child 13191 05a9929ee10e
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Fri May 31 07:53:37 2002 +0200
     1.2 +++ b/NEWS	Fri May 31 07:55:17 2002 +0200
     1.3 @@ -3,8 +3,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* arith(_tac) does now know about div 2 and mod 2 on type nat.
     1.8 -  It can solve simple goals like "0 < n ==> n div 2 < (n::nat)"
     1.9 +* arith(_tac) does now know about div k and mod k where k is a numeral of
    1.10 +  type nat. It can solve simple goals like "0 < n ==> n div 2 < (n::nat)"
    1.11    but fails if divisibility plays a role like in
    1.12    "n div 2 + (n+1) div 2 = (n::nat)".
    1.13  * simp's arithmetic capabilities have been enhanced a bit: