| Fri, 30 Sep 2016 15:51:43 +0200 |
hoelzl |
HOL-Analysis: fix latex generation
|
changeset |
files
|
| Fri, 30 Sep 2016 15:35:46 +0200 |
hoelzl |
Probability: fix proof
|
changeset |
files
|
| Fri, 30 Sep 2016 15:35:43 +0200 |
hoelzl |
Library: fix name Product_plus to Product_Plus
|
changeset |
files
|
| Fri, 30 Sep 2016 15:35:37 +0200 |
hoelzl |
HOL-Analysis: move Product_Vector and Inner_Product from Library
|
changeset |
files
|
| Fri, 30 Sep 2016 15:35:32 +0200 |
hoelzl |
HOL-Analysis: move Continuum_Not_Denumerable from Library
|
changeset |
files
|
| Fri, 30 Sep 2016 12:00:17 +0200 |
hoelzl |
HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
|
changeset |
files
|
| 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)
|
changeset |
files
|
| Fri, 30 Sep 2016 14:05:51 +0100 |
paulson |
new material on paths, etc. Also rationalisation
|
changeset |
files
|
| Fri, 30 Sep 2016 10:00:49 +0200 |
Manuel Eberl |
Merged
|
changeset |
files
|
| Thu, 29 Sep 2016 16:49:42 +0200 |
eberlm |
Set_Permutations replaced by more general Multiset_Permutations
|
changeset |
files
|
| Thu, 29 Sep 2016 20:54:46 +0200 |
boehmes |
CONTRIBUTORS: new proof method "argo"
|
changeset |
files
|
| Thu, 29 Sep 2016 20:54:45 +0200 |
boehmes |
NEWS: new proof method "argo"
|
changeset |
files
|