Merge
authorpaulson <lp15@cam.ac.uk>
Tue Oct 25 15:48:31 2016 +0100 (2016-10-25)
changeset 643956b57eb9e7790
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