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

Makarius makarius at sketis.net
Wed Jan 6 16:21:44 CET 2016


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


More information about the isabelle-dev mailing list