summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 08 Jul 1999 13:55:18 +0200 | |

changeset 6922 | f5c5b81b3f14 |

parent 6921 | 78a2ce8fb8df |

child 6923 | 51c415f15007 |

integer division

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