| author |
|---|
Chun Tian |
Measure, Lebesgue and Probability Theory for HOL4 (experimental version)
The main purpose is to port probability-related proof scripts from HVG concordia to HOL4 official, with my own additions.
See [https://github.com/HOL-Theorem-Prover/HOL/tree/develop/src/probability] for the official version.