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

author | wenzelm |

Mon, 10 Feb 2020 21:59:24 +0100 | |

changeset 71640 | b3954e1387b0 |

parent 71639 | 66a06a55c00c |

child 71641 | 182956c8e020 |

tuned;

--- a/NEWS Mon Feb 10 21:12:52 2020 +0100 +++ b/NEWS Mon Feb 10 21:59:24 2020 +0100 @@ -83,15 +83,15 @@ sign_simps and field_split_simps can be used instead of divide_simps. INCOMPATIBILITY. +* Theory HOL.Complete_Lattices: +renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf + * Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) associates to the left now as is customary. * Theory HOL-Library.Ramsey: full finite Ramsey's theorem with multiple colours and arbitrary exponents. -* Theory Complete_Lattices: -renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf - * Session HOL-Analysis: proof method "metric" implements a decision procedure for simple linear statements in metric spaces. @@ -114,9 +114,6 @@ project configuration for Isabelle/Scala/jEdit, to support Scala IDEs such as IntelliJ IDEA. -* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM -have been discontinued -- deprecated since Isabelle2018. - * The command-line tool "isabelle phabricator_setup" facilitates self-hosting of the Phabricator software-development platform, with support for Git, Mercurial, Subversion repositories. This helps to avoid @@ -142,6 +139,9 @@ inferences; it might help to reconstruct the formal structure of theory libraries. See also the module Export_Theory in Isabelle/Scala. +* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM +have been discontinued -- deprecated since Isabelle2018. + New in Isabelle2019 (June 2019)