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

author | paulson |

Fri, 24 Apr 1998 13:06:17 +0200 | |

changeset 4825 | e4e56a1bcbe2 |

parent 4824 | df8fc4626a9e |

child 4826 | 44d38b2737e2 |

tidied; div & mod

--- a/NEWS Fri Apr 24 11:22:39 1998 +0200 +++ b/NEWS Fri Apr 24 13:06:17 1998 +0200 @@ -40,15 +40,19 @@ * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset -* HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized - some theorems about n-1 +* HOL/Arithmetic + + - removed 'pred' (predecessor) function + + - generalized some theorems about n-1 + + - Many new laws about "div" and "mod" + + - New laws about greatest common divisors (see theory ex/Primes) * HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of "inverse" -* HOL/equalities: added many new laws involving unions, intersectinos, - difference, etc. - * recdef can now declare non-recursive functions, with {} supplied as the well-founded relation @@ -74,7 +78,7 @@ * new theory Vimage (inverse image of a function, syntax f-``B); -* many new identities for unions, intersections, etc.; +* many new identities for unions, intersections, set difference, etc.; New in Isabelle98 (January 1998)