[isabelle-dev] CONTRIBUTIONS: The central limit theorem is now in Isabelle
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.
> 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.
More information about the isabelle-dev