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

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)

new material on paths, etc. Also rationalisation

Merged

Set_Permutations replaced by more general Multiset_Permutations

CONTRIBUTORS: new proof method "argo"

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)