Mercurial
Mercurial
>
repos
>
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
src/HOL/Analysis/Complete_Measure.thy
Sun, 15 Apr 2018 13:57:00 +0100
paulson
various new results on measures, integrals, etc., and some simplified proofs
file
|
diff
|
annotate
Tue, 18 Oct 2016 12:01:54 +0200
hoelzl
HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
file
|
diff
|
annotate
Fri, 30 Sep 2016 11:35:39 +0200
hoelzl
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)
file
|
diff
|
annotate
Thu, 29 Sep 2016 18:52:34 +0200
hoelzl
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
file
|
diff
|
annotate
Thu, 29 Sep 2016 13:54:57 +0200
hoelzl
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
file
|
diff
|
annotate
Fri, 23 Sep 2016 18:34:34 +0200
hoelzl
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
file
|
diff
|
annotate
Fri, 23 Sep 2016 10:26:04 +0200
hoelzl
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
file
|
diff
|
annotate
Mon, 08 Aug 2016 14:13:14 +0200
hoelzl
rename HOL-Multivariate_Analysis to HOL-Analysis.
file
|
diff
|
annotate
|
base
less
more
(0)
tip