summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

invoke argo as part of the tried automatic proof methods

new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic

HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)

HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure

HOL-Analysis: move gauges and (tagged) divisions to its own theory file

HOL-Analysis: add cover lemma ported by L. C. Paulson

more new material

Generalised the type of map_poly

Merge

new material connected with HOL Light measure theory, plus more rationalisation