author | paulson |

Fri Aug 11 13:26:40 2000 +0200 (2000-08-11) | |

changeset 9577 | 9e66e8ed8237 |

parent 9576 | 3df14e0a3a51 |

child 9578 | ab26d6c8ebfe |

ZF arith

1.1 --- a/NEWS Fri Aug 11 10:34:02 2000 +0200 1.2 +++ b/NEWS Fri Aug 11 13:26:40 2000 +0200 1.3 @@ -269,16 +269,18 @@ 1.4 1.5 *** ZF *** 1.6 1.7 -* simplification automatically cancels common terms in arithmetic expressions over nat; 1.8 +* simplification automatically cancels common terms in arithmetic expressions 1.9 +over nat and int; 1.10 1.11 * new treatment of nat to minimize type-checking: all operators coerce their 1.12 operands to a natural number using the function natify, making the algebraic 1.13 laws unconditional; 1.14 1.15 -* as above, for int; 1.16 +* as above, for int: operators coerce their operands to an integer using the 1.17 +function intify; 1.18 1.19 * the integer library now contains many of the usual laws for the orderings, 1.20 -including $<=; 1.21 +including $<=, and monotonicity laws for $+ and $*; 1.22 1.23 1.24 *** FOL & ZF ***