author | wenzelm |

Sun Feb 11 13:26:23 2001 +0100 (2001-02-11) | |

changeset 11094 | b803ef642e60 |

parent 11093 | 62c2e0af1d30 |

child 11095 | 2ffaf1e1e101 |

tuned;

1.1 --- a/NEWS Sat Feb 10 08:52:41 2001 +0100 1.2 +++ b/NEWS Sun Feb 11 13:26:23 2001 +0100 1.3 @@ -7,12 +7,6 @@ 1.4 1.5 *** Overview of INCOMPATIBILITIES *** 1.6 1.7 -* HOL/Algebra: special summation operator SUM no longer exists, it has 1.8 -been replaced by setsum; infix 'assoc' now has priority 50 (like 'dvd'); 1.9 - 1.10 -* HOL/Algebra: axiom 'one_not_zero' has been moved from axclass 'ring' 1.11 -to 'domain', this makes the theory consistent with mathematical literature; 1.12 - 1.13 * HOL: inductive package no longer splits induction rule aggressively, 1.14 but only as far as specified by the introductions given; the old 1.15 format may recovered via ML function complete_split_rule or attribute 1.16 @@ -134,9 +128,15 @@ 1.17 modelling and verification task performed in Isabelle/HOL + 1.18 Isabelle/Isar + Isabelle document preparation (by Markus Wenzel). 1.19 1.20 +* HOL/Algebra: special summation operator SUM no longer exists, it has 1.21 +been replaced by setsum; infix 'assoc' now has priority 50 (like 1.22 +'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to 1.23 +'domain', this makes the theory consistent with mathematical 1.24 +literature; 1.25 + 1.26 * HOL basics: added overloaded operations "inverse" and "divide" 1.27 (infix "/"), syntax for generic "abs" operation, generic summation 1.28 -operator; 1.29 +operator \<Sum>; 1.30 1.31 * HOL/typedef: simplified package, provide more useful rules (see also 1.32 HOL/subset.thy); 1.33 @@ -154,7 +154,7 @@ 1.34 * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals 1.35 and Fleuriot's mechanization of analysis; 1.36 1.37 -* HOL-Real, HOL-Hyperreals: improved arithmetic simplification; 1.38 +* HOL/Real, HOL/Hyperreal: improved arithmetic simplification; 1.39 1.40 1.41 *** CTT ***