NEWS
changeset 13443 1c3327c348b3
parent 13425 119ae829ad9b
child 13459 83f41b047a39
     1.1 --- a/NEWS	Fri Aug 02 11:12:34 2002 +0200
     1.2 +++ b/NEWS	Fri Aug 02 11:49:55 2002 +0200
     1.3 @@ -28,16 +28,23 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* attribute [symmetric] now works for relations as well. It turns
     1.8 -  (x,y) : R^-1 into (y,x) : R, and vice versa.
     1.9 -
    1.10 -* arith(_tac) does now know about div k and mod k where k is a numeral of
    1.11 -  type nat or int. It can solve simple goals like
    1.12 +* 'typedef' command has new option "open" to suppress the set
    1.13 +definition;
    1.14 +
    1.15 +* attribute [symmetric] now works for relations as well; it turns
    1.16 +(x,y) : R^-1 into (y,x) : R, and vice versa;
    1.17 +
    1.18 +* arith(_tac) does now know about div k and mod k where k is a numeral
    1.19 +of type nat or int. It can solve simple goals like
    1.20 +
    1.21    "0 < n ==> n div 2 < (n::nat)"
    1.22 -  but fails if divisibility plays a role like in
    1.23 -  "n div 2 + (n+1) div 2 = (n::nat)".
    1.24 -* simp's arithmetic capabilities have been enhanced a bit:
    1.25 -  it now takes ~= in premises into account (by performing a case split).
    1.26 +
    1.27 +but fails if divisibility plays a role like in
    1.28 +
    1.29 +  "n div 2 + (n+1) div 2 = (n::nat)"
    1.30 +
    1.31 +* simp's arithmetic capabilities have been enhanced a bit: it now
    1.32 +takes ~= in premises into account (by performing a case split);
    1.33  
    1.34  
    1.35