summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Manuel Eberl <eberlm@in.tum.de> |

Wed, 27 Jul 2016 10:44:22 +0200 | |

changeset 63552 | 2112e5fe9712 |

parent 63551 | 679402a894ae |

child 63553 | 4a72b37ac4b8 |

NEWS: Primes

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

NEWS | file | annotate | diff | comparison | revisions |

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