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

author | wenzelm |

Wed, 27 May 2020 13:57:13 +0200 | |

changeset 71901 | 0408f6814224 |

parent 71900 | f08cf9d8f90b |

child 71902 | 1529336eaedc |

misc tuning;

--- a/NEWS Wed May 27 13:22:17 2020 +0200 +++ b/NEWS Wed May 27 13:57:13 2020 +0200 @@ -7,6 +7,31 @@ New in this Isabelle version ---------------------------- +*** Pure *** + +* Definitions in locales produce rule which can be added as congruence +rule to protect foundational terms during simplification. + + +*** HOL *** + +* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs" +on datatypes to "False" if either side is a proper subexpression of the +other (for any datatype with a reasonable size function). + +* New constant "power_int" for exponentiation with integer exponent, +written as "x powi n". + +* Added the "at most 1" quantifier, Uniq. + +* For the natural numbers, Sup{} = 0. + + +*** FOL *** + +* Added the "at most 1" quantifier, Uniq, as in HOL. + + *** System *** * The command-line tool "isabelle console" now supports interrupts @@ -34,23 +59,6 @@ directory (e.g. /var/www/phabricator-vcs/libphutil). -*** Pure *** - -* Definitions in locales produce rule which can be added as congruence -rule to protect foundational terms during simplification. - -*** HOL *** - -* New constant "power_int" for exponentiation with integer exponent, -written as "x powi n". - -* Added the "at most 1" quantifier, Uniq. - -* For the natural numbers, Sup{} = 0. - -*** FOL *** - -* Added the "at most 1" quantifier, Uniq, as in HOL. New in Isabelle2020 (April 2020) -------------------------------- @@ -464,10 +472,6 @@ *** HOL *** -* Simproc 'datatype_no_proper_subterm' rewrites equalities 'lhs = rhs' -on datatypes to 'False' if either side is a proper subexpression of the -other (for any datatype with a reasonable size function). - * Command 'export_code' produces output as logical files within the theory context, as well as formal session exports that can be materialized via command-line tools "isabelle export" or "isabelle build