#478 (Sep 29, 2016, 7:04:05 PM)

1. HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson) (detail / hgweb)
2. HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure (detail / hgweb)
3. HOL-Analysis: move gauges and (tagged) divisions to its own theory file (detail / hgweb)
4. HOL-Analysis: add cover lemma ported by L. C. Paulson (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 3 sec waiting;
• 1 hr 33 min build duration;
• 1 hr 38 min total from scheduled to completion.