--- 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:
--- 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
--- 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
#\<subseteq># ~> \<le>
#\<subset># ~> <
@@ -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 ***