*** empty log message ***
authornipkow
Thu Jul 11 09:31:01 2002 +0200 (2002-07-11)
changeset 13344c8eb3fbf4c0c
parent 13343 3b2b18c58d80
child 13345 bd611943cbc2
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Thu Jul 11 09:17:01 2002 +0200
     1.2 +++ b/NEWS	Thu Jul 11 09:31:01 2002 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -16,8 +15,12 @@
     1.9  
    1.10  *** HOL ***
    1.11  
    1.12 +* attribute [symmetric] now works for relations as well. It turns
    1.13 +  (x,y) : R^-1 into (y,x) : R, and vice versa.
    1.14 +
    1.15  * arith(_tac) does now know about div k and mod k where k is a numeral of
    1.16 -  type nat. It can solve simple goals like "0 < n ==> n div 2 < (n::nat)"
    1.17 +  type nat or int. It can solve simple goals like
    1.18 +  "0 < n ==> n div 2 < (n::nat)"
    1.19    but fails if divisibility plays a role like in
    1.20    "n div 2 + (n+1) div 2 = (n::nat)".
    1.21  * simp's arithmetic capabilities have been enhanced a bit: