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

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

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

added lemma;

Trying out "subgoal", and no more [| |]

HOL-Analysis: fix latex generation

Probability: fix proof

Library: fix name Product_plus to Product_Plus

HOL-Analysis: move Product_Vector and Inner_Product from Library

HOL-Analysis: move Continuum_Not_Denumerable from Library

HOL-Analysis: move Library/Convex to Convex_Euclidean_Space

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)

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

sequential (jobs = 1) makeall profile

syntactic type class for operation mod named after mod;
simplified assumptions of type class semiring_div

dropped tautological pattern

more warning comments

more lemmas