Fri, 30 Sep 2016 15:35:32 +0200 | hoelzl | HOL-Analysis: move Continuum_Not_Denumerable from Library | changeset | files |
Fri, 30 Sep 2016 12:00:17 +0200 | hoelzl | HOL-Analysis: move Library/Convex to Convex_Euclidean_Space | changeset | files |
Fri, 30 Sep 2016 11:35:39 +0200 | hoelzl | HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson) | changeset | files |