summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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