#156 (Sep 30, 2016, 12:50:07 AM)

1. CONTRIBUTORS: new proof method "argo" (detail / hgweb)
2. NEWS: new proof method "argo" (detail / hgweb)
3. use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable (detail / hgweb)
4. invoke argo as part of the tried automatic proof methods (detail / hgweb)
5. new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic (detail / hgweb)
6. HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson) (detail / hgweb)
7. HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure (detail / hgweb)
8. HOL-Analysis: move gauges and (tagged) divisions to its own theory file (detail / hgweb)
9. HOL-Analysis: add cover lemma ported by L. C. Paulson (detail / hgweb)
10. more new material (detail / hgweb)
11. Generalised the type of map_poly (detail / hgweb)

Started by an SCM change

This run spent:

• 5.6 sec waiting;
• 1 hr 16 min build duration;
• 1 hr 16 min total from scheduled to completion.