# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1469609062 -7200
# Node ID 2112e5fe9712ab737380c128c4568b536abf7008
# Parent  679402a894aeff991c7a7945f75432cd9a01b9d8
NEWS: Primes

diff -r 679402a894ae -r 2112e5fe9712 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Jul 26 14:29:20 2016 +0200
+++ b/CONTRIBUTORS	Wed Jul 27 10:44:22 2016 +0200
@@ -17,12 +17,19 @@
   Reasoning support for monotonicity, continuity and
   admissibility in chain-complete partial orders.
 
+* May 2016: Manuel Eberl
+  Code generation for Probability Mass Functions.
+
 * June 2016: Andreas Lochbihler
   Formalisation of discrete subprobability distributions.
 
 * 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
+
 Contributions to Isabelle2016
 -----------------------------
 
diff -r 679402a894ae -r 2112e5fe9712 NEWS
--- a/NEWS	Tue Jul 26 14:29:20 2016 +0200
+++ b/NEWS	Wed Jul 27 10:44:22 2016 +0200
@@ -173,6 +173,14 @@
 
 *** HOL ***
 
+* Number_Theory: algebraic foundation for primes: Introduction of 
+predicates "is_prime", "irreducible", a "prime_factorization" 
+function, the "factorial_ring" typeclass with instance proofs for 
+nat, int, poly.
+
+* Probability: Code generation and QuickCheck for Probability Mass 
+Functions.
+
 * Theory Set_Interval.thy: substantial new theorems on indexed sums
 and products.