NEWS: Primes
authorManuel Eberl <eberlm@in.tum.de>
Wed Jul 27 10:44:22 2016 +0200 (2016-07-27)
changeset 635522112e5fe9712
parent 63551 679402a894ae
child 63553 4a72b37ac4b8
NEWS: Primes
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Jul 26 14:29:20 2016 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Jul 27 10:44:22 2016 +0200
     1.3 @@ -17,12 +17,19 @@
     1.4    Reasoning support for monotonicity, continuity and
     1.5    admissibility in chain-complete partial orders.
     1.6  
     1.7 +* May 2016: Manuel Eberl
     1.8 +  Code generation for Probability Mass Functions.
     1.9 +
    1.10  * June 2016: Andreas Lochbihler
    1.11    Formalisation of discrete subprobability distributions.
    1.12  
    1.13  * July 2016: Daniel Stuewe
    1.14    Height-size proofs in HOL/Data_Structures
    1.15  
    1.16 +* July 2016: Manuel Eberl
    1.17 +  Algebraic foundation for primes; generalization from nat
    1.18 +  to general factorial rings
    1.19 +
    1.20  Contributions to Isabelle2016
    1.21  -----------------------------
    1.22  
     2.1 --- a/NEWS	Tue Jul 26 14:29:20 2016 +0200
     2.2 +++ b/NEWS	Wed Jul 27 10:44:22 2016 +0200
     2.3 @@ -173,6 +173,14 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Number_Theory: algebraic foundation for primes: Introduction of 
     2.8 +predicates "is_prime", "irreducible", a "prime_factorization" 
     2.9 +function, the "factorial_ring" typeclass with instance proofs for 
    2.10 +nat, int, poly.
    2.11 +
    2.12 +* Probability: Code generation and QuickCheck for Probability Mass 
    2.13 +Functions.
    2.14 +
    2.15  * Theory Set_Interval.thy: substantial new theorems on indexed sums
    2.16  and products.
    2.17