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

NEWS

changeset 6922 | f5c5b81b3f14 |

parent 6795 | 35f214e73668 |

child 6925 | 8d4d45ec6a3d |

--- a/NEWS Thu Jul 08 13:48:11 1999 +0200 +++ b/NEWS Thu Jul 08 13:55:18 1999 +0200 @@ -7,6 +7,11 @@ *** Overview of INCOMPATIBILITIES (see below for more details) *** +* HOL: The THEN and ELSE parts of conditional expressions (if P then x else y) +are no longer simplified. (This allows the simplifier to unfold recursive +functional programs.) To restore the old behaviour, declare + Delcongs [if_weak_cong]; + * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement; @@ -102,6 +107,11 @@ nat/int formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'. +* Integer division and remainder can now be performed on constant arguments. + +* Many properties of integer multiplication, division and remainder are now +available. + * New bounded quantifier syntax (input only): ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P