tuned and updated for release;
authorwenzelm
Tue Oct 25 12:36:09 2016 +0200 (2016-10-25)
changeset 6439317a7543fadad
parent 64392 9456313b57ed
child 64395 6b57eb9e7790
child 64397 6e9c22c494c5
tuned and updated for release;
CONTRIBUTORS
     1.1 --- a/CONTRIBUTORS	Tue Oct 25 12:23:54 2016 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Oct 25 12:36:09 2016 +0200
     1.3 @@ -6,50 +6,54 @@
     1.4  Contributions to Isabelle2016-1
     1.5  -------------------------------
     1.6  
     1.7 -* January 2016: Florian Haftmann, TUM
     1.8 -  Abolition of compound operators INFIMUM and SUPREMUM
     1.9 -  for complete lattices.
    1.10 +* October 2016: Jasmin Blanchette
    1.11 +  Integration of Nunchaku model finder.
    1.12 +
    1.13 +* October 2016: Jaime Mendizabal Roche, TUM
    1.14 +  Ported remaining theories of session Old_Number_Theory to the new
    1.15 +  Number_Theory and removed Old_Number_Theory.
    1.16 +
    1.17 +* September 2016: Sascha Boehme
    1.18 +  Proof method "argo" based on SMT technology for a combination of
    1.19 +  quantifier-free propositional logic, equality and linear real arithmetic
    1.20 +
    1.21 +* July 2016: Daniel Stuewe
    1.22 +  Height-size proofs in HOL-Data_Structures.
    1.23 +
    1.24 +* July 2016: Manuel Eberl, TUM
    1.25 +  Algebraic foundation for primes; generalization from nat to general
    1.26 +  factorial rings.
    1.27 +
    1.28 +* June 2016: Andreas Lochbihler, ETH Zurich
    1.29 +  Formalisation of discrete subprobability distributions.
    1.30 +
    1.31 +* June 2016: Florian Haftmann, TUM
    1.32 +  Improvements to code generation: optional timing measurements, more succint
    1.33 +  closures for static evaluation, less ambiguities concering Scala implicits.
    1.34 +
    1.35 +* May 2016: Manuel Eberl, TUM
    1.36 +  Code generation for Probability Mass Functions.
    1.37  
    1.38  * March 2016: Florian Haftmann, TUM
    1.39    Abstract factorial rings with unique factorization.
    1.40  
    1.41  * March 2016: Florian Haftmann, TUM
    1.42 -  Reworking of the HOL char type as special case of a
    1.43 -  finite numeral type.
    1.44 -
    1.45 -* March 2016: Andreas Lochbihler
    1.46 -  Reasoning support for monotonicity, continuity and
    1.47 -  admissibility in chain-complete partial orders.
    1.48 +  Reworking of the HOL char type as special case of a finite numeral type.
    1.49  
    1.50 -* May 2016: Manuel Eberl
    1.51 -  Code generation for Probability Mass Functions.
    1.52 -
    1.53 -* June 2016: Andreas Lochbihler
    1.54 -  Formalisation of discrete subprobability distributions.
    1.55 -
    1.56 -* June 2016: Florian Haftmann, TUM
    1.57 -  Improvements to code generation: optional timing measurements,
    1.58 -  more succint closures for static evaluation, less ambiguities
    1.59 -  concering Scala implicits.
    1.60 +* March 2016: Andreas Lochbihler, ETH Zurich
    1.61 +  Reasoning support for monotonicity, continuity and admissibility in
    1.62 +  chain-complete partial orders.
    1.63  
    1.64 -* July 2016: Daniel Stuewe
    1.65 -  Height-size proofs in HOL/Data_Structures
    1.66 -
    1.67 -* July 2016: Manuel Eberl
    1.68 -  Algebraic foundation for primes; generalization from nat
    1.69 -  to general factorial rings
    1.70 +* February - October 2016: Makarius Wenzel
    1.71 +  Prover IDE improvements.
    1.72 +  ML IDE improvements: bootstrap of Pure.
    1.73 +  Isar language consolidation.
    1.74 +  Notational modernization of HOL.
    1.75 +  Tight Poly/ML integration.
    1.76 +  More Isabelle/Scala system programming modules (e.g. SSH, Mercurial).
    1.77  
    1.78 -* September 2016: Sascha Boehme
    1.79 -  Proof method 'argo' based on SMT technology for a combination of
    1.80 -  quantifier-free propositional logic, equality and linear real
    1.81 -  arithmetic
    1.82 -
    1.83 -* October 2016: Jaime Mendizabal Roche
    1.84 -  Ported remaining theories of Old_Number_Theory to the new 
    1.85 -  Number_Theory and removed Old_Number_Theory.
    1.86 -
    1.87 -* October 2016: Jasmin Blanchette
    1.88 -  Integration of Nunchaku model finder.
    1.89 +* January 2016: Florian Haftmann, TUM
    1.90 +  Abolition of compound operators INFIMUM and SUPREMUM for complete lattices.
    1.91  
    1.92  
    1.93  Contributions to Isabelle2016