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
```