This is certainly a must! Thanks! Larry > On 4 Jan 2016, at 19:48, Johannes Hölzl <hoelzl at in.tum.de> wrote: > > I'm currently cleaning up the Central Limit Theorem, and I want to it > entirely to HOL-Probability. > > I hope to finish this in 1 week, to get it into Isabelle 2016.