--- 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
-----------------------------
--- 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.