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

author | wenzelm |

Sun, 11 Feb 2001 13:26:23 +0100 | |

changeset 11094 | b803ef642e60 |

parent 11093 | 62c2e0af1d30 |

child 11095 | 2ffaf1e1e101 |

tuned;

--- a/NEWS Sat Feb 10 08:52:41 2001 +0100 +++ b/NEWS Sun Feb 11 13:26:23 2001 +0100 @@ -7,12 +7,6 @@ *** Overview of INCOMPATIBILITIES *** -* HOL/Algebra: special summation operator SUM no longer exists, it has -been replaced by setsum; infix 'assoc' now has priority 50 (like 'dvd'); - -* HOL/Algebra: axiom 'one_not_zero' has been moved from axclass 'ring' -to 'domain', this makes the theory consistent with mathematical literature; - * HOL: inductive package no longer splits induction rule aggressively, but only as far as specified by the introductions given; the old format may recovered via ML function complete_split_rule or attribute @@ -134,9 +128,15 @@ modelling and verification task performed in Isabelle/HOL + Isabelle/Isar + Isabelle document preparation (by Markus Wenzel). +* HOL/Algebra: special summation operator SUM no longer exists, it has +been replaced by setsum; infix 'assoc' now has priority 50 (like +'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to +'domain', this makes the theory consistent with mathematical +literature; + * HOL basics: added overloaded operations "inverse" and "divide" (infix "/"), syntax for generic "abs" operation, generic summation -operator; +operator \<Sum>; * HOL/typedef: simplified package, provide more useful rules (see also HOL/subset.thy); @@ -154,7 +154,7 @@ * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and Fleuriot's mechanization of analysis; -* HOL-Real, HOL-Hyperreals: improved arithmetic simplification; +* HOL/Real, HOL/Hyperreal: improved arithmetic simplification; *** CTT ***