summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 13443 | 1c3327c348b3 |

parent 13425 | 119ae829ad9b |

child 13459 | 83f41b047a39 |

--- a/NEWS Fri Aug 02 11:12:34 2002 +0200 +++ b/NEWS Fri Aug 02 11:49:55 2002 +0200 @@ -28,16 +28,23 @@ *** HOL *** -* attribute [symmetric] now works for relations as well. It turns - (x,y) : R^-1 into (y,x) : R, and vice versa. - -* arith(_tac) does now know about div k and mod k where k is a numeral of - type nat or int. It can solve simple goals like +* 'typedef' command has new option "open" to suppress the set +definition; + +* attribute [symmetric] now works for relations as well; it turns +(x,y) : R^-1 into (y,x) : R, and vice versa; + +* arith(_tac) does now know about div k and mod k where k is a numeral +of type nat or int. It can solve simple goals like + "0 < n ==> n div 2 < (n::nat)" - but fails if divisibility plays a role like in - "n div 2 + (n+1) div 2 = (n::nat)". -* simp's arithmetic capabilities have been enhanced a bit: - it now takes ~= in premises into account (by performing a case split). + +but fails if divisibility plays a role like in + + "n div 2 + (n+1) div 2 = (n::nat)" + +* simp's arithmetic capabilities have been enhanced a bit: it now +takes ~= in premises into account (by performing a case split);