# HG changeset patch # User paulson # Date 1477406911 -3600 # Node ID 6b57eb9e779052c5ec6b6b4fe14f3521f4fe4845 # Parent 141e1ed8d5a011fe812bfb38cc88d96c0f4f398b# Parent 17a7543fadada3f65bd15f245a0bc0dd81ea4a7c Merge diff -r 141e1ed8d5a0 -r 6b57eb9e7790 ANNOUNCE --- a/ANNOUNCE Tue Oct 25 15:46:07 2016 +0100 +++ b/ANNOUNCE Tue Oct 25 15:48:31 2016 +0100 @@ -3,11 +3,27 @@ Isabelle2016-1 is now available. -This version introduces significant changes over Isabelle2016, see the -NEWS file in the distribution for further details. Some highlights are -as follows: +This version introduces significant changes over Isabelle2016: see the NEWS +file for further details. Some notable points are as follows: + +* Improved Isabelle/jEdit Prover IDE: more support for formal text structure, +more visual feedback. + +* The Isabelle/ML IDE can load Isabelle/Pure into itself. + +* Improved Isar proof and specification elements. -* TBA +* HOL codatatype specifications: new commands for corecursive functions. + +* HOL tools: new Argo SMT solver, experimental Nunchaku model finder. + +* HOL library: improved HOL-Number_Theory and HOL-Library, especially theory +Multiset. + +* Reorganization of HOL-Probability versus and HOL-Analysis, with many new +theorems ported from HOL-Light. + +* Improved management of Poly/ML 5.6 processes and cumulative heap files. You may get Isabelle2016-1 from the following mirror sites: diff -r 141e1ed8d5a0 -r 6b57eb9e7790 CONTRIBUTORS --- a/CONTRIBUTORS Tue Oct 25 15:46:07 2016 +0100 +++ b/CONTRIBUTORS Tue Oct 25 15:48:31 2016 +0100 @@ -6,50 +6,54 @@ Contributions to Isabelle2016-1 ------------------------------- -* January 2016: Florian Haftmann, TUM - Abolition of compound operators INFIMUM and SUPREMUM - for complete lattices. +* October 2016: Jasmin Blanchette + Integration of Nunchaku model finder. + +* October 2016: Jaime Mendizabal Roche, TUM + Ported remaining theories of session Old_Number_Theory to the new + Number_Theory and removed Old_Number_Theory. + +* September 2016: Sascha Boehme + Proof method "argo" based on SMT technology for a combination of + quantifier-free propositional logic, equality and linear real arithmetic + +* July 2016: Daniel Stuewe + Height-size proofs in HOL-Data_Structures. + +* July 2016: Manuel Eberl, TUM + Algebraic foundation for primes; generalization from nat to general + factorial rings. + +* June 2016: Andreas Lochbihler, ETH Zurich + Formalisation of discrete subprobability distributions. + +* June 2016: Florian Haftmann, TUM + Improvements to code generation: optional timing measurements, more succint + closures for static evaluation, less ambiguities concering Scala implicits. + +* May 2016: Manuel Eberl, TUM + Code generation for Probability Mass Functions. * March 2016: Florian Haftmann, TUM Abstract factorial rings with unique factorization. * March 2016: Florian Haftmann, TUM - Reworking of the HOL char type as special case of a - finite numeral type. - -* March 2016: Andreas Lochbihler - Reasoning support for monotonicity, continuity and - admissibility in chain-complete partial orders. + Reworking of the HOL char type as special case of a finite numeral type. -* May 2016: Manuel Eberl - Code generation for Probability Mass Functions. - -* June 2016: Andreas Lochbihler - Formalisation of discrete subprobability distributions. - -* June 2016: Florian Haftmann, TUM - Improvements to code generation: optional timing measurements, - more succint closures for static evaluation, less ambiguities - concering Scala implicits. +* March 2016: Andreas Lochbihler, ETH Zurich + Reasoning support for monotonicity, continuity and admissibility in + chain-complete partial orders. -* July 2016: Daniel Stuewe - Height-size proofs in HOL/Data_Structures - -* July 2016: Manuel Eberl - Algebraic foundation for primes; generalization from nat - to general factorial rings +* February - October 2016: Makarius Wenzel + Prover IDE improvements. + ML IDE improvements: bootstrap of Pure. + Isar language consolidation. + Notational modernization of HOL. + Tight Poly/ML integration. + More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). -* September 2016: Sascha Boehme - Proof method 'argo' based on SMT technology for a combination of - quantifier-free propositional logic, equality and linear real - arithmetic - -* October 2016: Jaime Mendizabal Roche - Ported remaining theories of Old_Number_Theory to the new - Number_Theory and removed Old_Number_Theory. - -* October 2016: Jasmin Blanchette - Integration of Nunchaku model finder. +* January 2016: Florian Haftmann, TUM + Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. Contributions to Isabelle2016 diff -r 141e1ed8d5a0 -r 6b57eb9e7790 NEWS --- a/NEWS Tue Oct 25 15:46:07 2016 +0100 +++ b/NEWS Tue Oct 25 15:48:31 2016 +0100 @@ -470,6 +470,34 @@ * Added class topological_monoid. +* The following theorems have been renamed: + + setsum_left_distrib ~> setsum_distrib_right + setsum_right_distrib ~> setsum_distrib_left + +INCOMPATIBILITY. + +* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. +INCOMPATIBILITY. + +* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional +comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` +A)". + +* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. + +* The type class ordered_comm_monoid_add is now called +ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add +is introduced as the combination of ordered_ab_semigroup_add + +comm_monoid_add. INCOMPATIBILITY. + +* Introduced the type classes canonically_ordered_comm_monoid_add and +dioid. + +* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When +instantiating linordered_semiring_strict and ordered_ab_group_add, an +explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might +be required. INCOMPATIBILITY. * Dropped various legacy fact bindings, whose replacements are often of a more general type also: @@ -646,16 +674,6 @@ * Session HOL-Probability: theory SPMF formalises discrete subprobability distributions. -* Session HOL-Number_Theory: algebraic foundation for primes: -Generalisation of predicate "prime" and introduction of predicates -"prime_elem", "irreducible", a "prime_factorization" function, and the -"factorial_ring" typeclass with instance proofs for nat, int, poly. Some -theorems now have different names, most notably "prime_def" is now -"prime_nat_iff". INCOMPATIBILITY. - -* Session Old_Number_Theory has been removed, after porting remaining -theories. - * Session HOL-Library: the names of multiset theorems have been normalised to distinguish which ordering the theorems are about @@ -685,35 +703,6 @@ Some functions have been renamed: ms_lesseq_impl -> subset_eq_mset_impl -* The following theorems have been renamed: - - setsum_left_distrib ~> setsum_distrib_right - setsum_right_distrib ~> setsum_distrib_left - -INCOMPATIBILITY. - -* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. -INCOMPATIBILITY. - -* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional -comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` -A)". - -* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. - -* The type class ordered_comm_monoid_add is now called -ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add -is introduced as the combination of ordered_ab_semigroup_add + -comm_monoid_add. INCOMPATIBILITY. - -* Introduced the type classes canonically_ordered_comm_monoid_add and -dioid. - -* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When -instantiating linordered_semiring_strict and ordered_ab_group_add, an -explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might -be required. INCOMPATIBILITY. - * HOL-Library: multisets are now ordered with the multiset ordering #\# ~> \ #\# ~> < @@ -886,7 +875,7 @@ empty_inter [simp] ~> [] INCOMPATIBILITY. -* Session HOL-Library, theory Multiset: The order of the variables in +* Session HOL-Library, theory Multiset: the order of the variables in the second cases of multiset_induct, multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A). INCOMPATIBILITY. @@ -933,6 +922,16 @@ Added theory of longest common prefixes. +* Session HOL-Number_Theory: algebraic foundation for primes: +Generalisation of predicate "prime" and introduction of predicates +"prime_elem", "irreducible", a "prime_factorization" function, and the +"factorial_ring" typeclass with instance proofs for nat, int, poly. Some +theorems now have different names, most notably "prime_def" is now +"prime_nat_iff". INCOMPATIBILITY. + +* Session Old_Number_Theory has been removed, after porting remaining +theories. + *** ML ***