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

NEWS: new proof method "argo"

use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable

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