[isabelle-dev] CONTRIBUTIONS: The central limit theorem is now in Isabelle

[Makarius]

On Wed, 6 Jan 2016, Johannes Hölzl wrote:

> The central limit theorem is now in the Isabelle repository:
>
> * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
>  Proof of the central limit theorem: includes weak convergence, characteristic
>  functions, and Levy's uniqueness and continuity theorem.
>
> http://isabelle.in.tum.de/repos/isabelle/rev/7582b39f51ed
>
>
> Besides this I do not have any further contributions for the Isabelle 2016 release.

Great.  I am impressed how much new material has emerged in the past few 
days.  Now we only need to wait one more week for Larry, and two more 
weeks for Oracle.


 	Makarius