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

author | paulson |

Fri, 11 Aug 2000 13:26:40 +0200 | |

changeset 9577 | 9e66e8ed8237 |

parent 9576 | 3df14e0a3a51 |

child 9578 | ab26d6c8ebfe |

ZF arith

--- a/NEWS Fri Aug 11 10:34:02 2000 +0200 +++ b/NEWS Fri Aug 11 13:26:40 2000 +0200 @@ -269,16 +269,18 @@ *** ZF *** -* simplification automatically cancels common terms in arithmetic expressions over nat; +* simplification automatically cancels common terms in arithmetic expressions +over nat and int; * new treatment of nat to minimize type-checking: all operators coerce their operands to a natural number using the function natify, making the algebraic laws unconditional; -* as above, for int; +* as above, for int: operators coerce their operands to an integer using the +function intify; * the integer library now contains many of the usual laws for the orderings, -including $<=; +including $<=, and monotonicity laws for $+ and $*; *** FOL & ZF ***