author | paulson <lp15@cam.ac.uk> |

Tue Oct 25 15:48:31 2016 +0100 (2016-10-25) | |

changeset 64395 | 6b57eb9e7790 |

parent 64394 | 141e1ed8d5a0 |

parent 64393 | 17a7543fadad |

child 64396 | 3f4a86c9d2b5 |

Merge

1.1 --- a/ANNOUNCE Tue Oct 25 15:46:07 2016 +0100 1.2 +++ b/ANNOUNCE Tue Oct 25 15:48:31 2016 +0100 1.3 @@ -3,11 +3,27 @@ 1.4 1.5 Isabelle2016-1 is now available. 1.6 1.7 -This version introduces significant changes over Isabelle2016, see the 1.8 -NEWS file in the distribution for further details. Some highlights are 1.9 -as follows: 1.10 +This version introduces significant changes over Isabelle2016: see the NEWS 1.11 +file for further details. Some notable points are as follows: 1.12 + 1.13 +* Improved Isabelle/jEdit Prover IDE: more support for formal text structure, 1.14 +more visual feedback. 1.15 + 1.16 +* The Isabelle/ML IDE can load Isabelle/Pure into itself. 1.17 + 1.18 +* Improved Isar proof and specification elements. 1.19 1.20 -* TBA 1.21 +* HOL codatatype specifications: new commands for corecursive functions. 1.22 + 1.23 +* HOL tools: new Argo SMT solver, experimental Nunchaku model finder. 1.24 + 1.25 +* HOL library: improved HOL-Number_Theory and HOL-Library, especially theory 1.26 +Multiset. 1.27 + 1.28 +* Reorganization of HOL-Probability versus and HOL-Analysis, with many new 1.29 +theorems ported from HOL-Light. 1.30 + 1.31 +* Improved management of Poly/ML 5.6 processes and cumulative heap files. 1.32 1.33 1.34 You may get Isabelle2016-1 from the following mirror sites:

2.1 --- a/CONTRIBUTORS Tue Oct 25 15:46:07 2016 +0100 2.2 +++ b/CONTRIBUTORS Tue Oct 25 15:48:31 2016 +0100 2.3 @@ -6,50 +6,54 @@ 2.4 Contributions to Isabelle2016-1 2.5 ------------------------------- 2.6 2.7 -* January 2016: Florian Haftmann, TUM 2.8 - Abolition of compound operators INFIMUM and SUPREMUM 2.9 - for complete lattices. 2.10 +* October 2016: Jasmin Blanchette 2.11 + Integration of Nunchaku model finder. 2.12 + 2.13 +* October 2016: Jaime Mendizabal Roche, TUM 2.14 + Ported remaining theories of session Old_Number_Theory to the new 2.15 + Number_Theory and removed Old_Number_Theory. 2.16 + 2.17 +* September 2016: Sascha Boehme 2.18 + Proof method "argo" based on SMT technology for a combination of 2.19 + quantifier-free propositional logic, equality and linear real arithmetic 2.20 + 2.21 +* July 2016: Daniel Stuewe 2.22 + Height-size proofs in HOL-Data_Structures. 2.23 + 2.24 +* July 2016: Manuel Eberl, TUM 2.25 + Algebraic foundation for primes; generalization from nat to general 2.26 + factorial rings. 2.27 + 2.28 +* June 2016: Andreas Lochbihler, ETH Zurich 2.29 + Formalisation of discrete subprobability distributions. 2.30 + 2.31 +* June 2016: Florian Haftmann, TUM 2.32 + Improvements to code generation: optional timing measurements, more succint 2.33 + closures for static evaluation, less ambiguities concering Scala implicits. 2.34 + 2.35 +* May 2016: Manuel Eberl, TUM 2.36 + Code generation for Probability Mass Functions. 2.37 2.38 * March 2016: Florian Haftmann, TUM 2.39 Abstract factorial rings with unique factorization. 2.40 2.41 * March 2016: Florian Haftmann, TUM 2.42 - Reworking of the HOL char type as special case of a 2.43 - finite numeral type. 2.44 - 2.45 -* March 2016: Andreas Lochbihler 2.46 - Reasoning support for monotonicity, continuity and 2.47 - admissibility in chain-complete partial orders. 2.48 + Reworking of the HOL char type as special case of a finite numeral type. 2.49 2.50 -* May 2016: Manuel Eberl 2.51 - Code generation for Probability Mass Functions. 2.52 - 2.53 -* June 2016: Andreas Lochbihler 2.54 - Formalisation of discrete subprobability distributions. 2.55 - 2.56 -* June 2016: Florian Haftmann, TUM 2.57 - Improvements to code generation: optional timing measurements, 2.58 - more succint closures for static evaluation, less ambiguities 2.59 - concering Scala implicits. 2.60 +* March 2016: Andreas Lochbihler, ETH Zurich 2.61 + Reasoning support for monotonicity, continuity and admissibility in 2.62 + chain-complete partial orders. 2.63 2.64 -* July 2016: Daniel Stuewe 2.65 - Height-size proofs in HOL/Data_Structures 2.66 - 2.67 -* July 2016: Manuel Eberl 2.68 - Algebraic foundation for primes; generalization from nat 2.69 - to general factorial rings 2.70 +* February - October 2016: Makarius Wenzel 2.71 + Prover IDE improvements. 2.72 + ML IDE improvements: bootstrap of Pure. 2.73 + Isar language consolidation. 2.74 + Notational modernization of HOL. 2.75 + Tight Poly/ML integration. 2.76 + More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). 2.77 2.78 -* September 2016: Sascha Boehme 2.79 - Proof method 'argo' based on SMT technology for a combination of 2.80 - quantifier-free propositional logic, equality and linear real 2.81 - arithmetic 2.82 - 2.83 -* October 2016: Jaime Mendizabal Roche 2.84 - Ported remaining theories of Old_Number_Theory to the new 2.85 - Number_Theory and removed Old_Number_Theory. 2.86 - 2.87 -* October 2016: Jasmin Blanchette 2.88 - Integration of Nunchaku model finder. 2.89 +* January 2016: Florian Haftmann, TUM 2.90 + Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. 2.91 2.92 2.93 Contributions to Isabelle2016

3.1 --- a/NEWS Tue Oct 25 15:46:07 2016 +0100 3.2 +++ b/NEWS Tue Oct 25 15:48:31 2016 +0100 3.3 @@ -470,6 +470,34 @@ 3.4 3.5 * Added class topological_monoid. 3.6 3.7 +* The following theorems have been renamed: 3.8 + 3.9 + setsum_left_distrib ~> setsum_distrib_right 3.10 + setsum_right_distrib ~> setsum_distrib_left 3.11 + 3.12 +INCOMPATIBILITY. 3.13 + 3.14 +* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. 3.15 +INCOMPATIBILITY. 3.16 + 3.17 +* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional 3.18 +comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` 3.19 +A)". 3.20 + 3.21 +* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 3.22 + 3.23 +* The type class ordered_comm_monoid_add is now called 3.24 +ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 3.25 +is introduced as the combination of ordered_ab_semigroup_add + 3.26 +comm_monoid_add. INCOMPATIBILITY. 3.27 + 3.28 +* Introduced the type classes canonically_ordered_comm_monoid_add and 3.29 +dioid. 3.30 + 3.31 +* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 3.32 +instantiating linordered_semiring_strict and ordered_ab_group_add, an 3.33 +explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 3.34 +be required. INCOMPATIBILITY. 3.35 3.36 * Dropped various legacy fact bindings, whose replacements are often 3.37 of a more general type also: 3.38 @@ -646,16 +674,6 @@ 3.39 * Session HOL-Probability: theory SPMF formalises discrete 3.40 subprobability distributions. 3.41 3.42 -* Session HOL-Number_Theory: algebraic foundation for primes: 3.43 -Generalisation of predicate "prime" and introduction of predicates 3.44 -"prime_elem", "irreducible", a "prime_factorization" function, and the 3.45 -"factorial_ring" typeclass with instance proofs for nat, int, poly. Some 3.46 -theorems now have different names, most notably "prime_def" is now 3.47 -"prime_nat_iff". INCOMPATIBILITY. 3.48 - 3.49 -* Session Old_Number_Theory has been removed, after porting remaining 3.50 -theories. 3.51 - 3.52 * Session HOL-Library: the names of multiset theorems have been 3.53 normalised to distinguish which ordering the theorems are about 3.54 3.55 @@ -685,35 +703,6 @@ 3.56 Some functions have been renamed: 3.57 ms_lesseq_impl -> subset_eq_mset_impl 3.58 3.59 -* The following theorems have been renamed: 3.60 - 3.61 - setsum_left_distrib ~> setsum_distrib_right 3.62 - setsum_right_distrib ~> setsum_distrib_left 3.63 - 3.64 -INCOMPATIBILITY. 3.65 - 3.66 -* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. 3.67 -INCOMPATIBILITY. 3.68 - 3.69 -* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional 3.70 -comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` 3.71 -A)". 3.72 - 3.73 -* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 3.74 - 3.75 -* The type class ordered_comm_monoid_add is now called 3.76 -ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 3.77 -is introduced as the combination of ordered_ab_semigroup_add + 3.78 -comm_monoid_add. INCOMPATIBILITY. 3.79 - 3.80 -* Introduced the type classes canonically_ordered_comm_monoid_add and 3.81 -dioid. 3.82 - 3.83 -* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 3.84 -instantiating linordered_semiring_strict and ordered_ab_group_add, an 3.85 -explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 3.86 -be required. INCOMPATIBILITY. 3.87 - 3.88 * HOL-Library: multisets are now ordered with the multiset ordering 3.89 #\<subseteq># ~> \<le> 3.90 #\<subset># ~> < 3.91 @@ -886,7 +875,7 @@ 3.92 empty_inter [simp] ~> [] 3.93 INCOMPATIBILITY. 3.94 3.95 -* Session HOL-Library, theory Multiset: The order of the variables in 3.96 +* Session HOL-Library, theory Multiset: the order of the variables in 3.97 the second cases of multiset_induct, multiset_induct2_size, 3.98 multiset_induct2 has been changed (e.g. Add A a ~> Add a A). 3.99 INCOMPATIBILITY. 3.100 @@ -933,6 +922,16 @@ 3.101 3.102 Added theory of longest common prefixes. 3.103 3.104 +* Session HOL-Number_Theory: algebraic foundation for primes: 3.105 +Generalisation of predicate "prime" and introduction of predicates 3.106 +"prime_elem", "irreducible", a "prime_factorization" function, and the 3.107 +"factorial_ring" typeclass with instance proofs for nat, int, poly. Some 3.108 +theorems now have different names, most notably "prime_def" is now 3.109 +"prime_nat_iff". INCOMPATIBILITY. 3.110 + 3.111 +* Session Old_Number_Theory has been removed, after porting remaining 3.112 +theories. 3.113 + 3.114 3.115 *** ML *** 3.116