hoelzl [Fri, 30 Sep 2016 15:35:46 +0200] rev 63973
Probability: fix proof
hoelzl [Fri, 30 Sep 2016 15:35:43 +0200] rev 63972
Library: fix name Product_plus to Product_Plus
hoelzl [Fri, 30 Sep 2016 15:35:37 +0200] rev 63971
HOL-Analysis: move Product_Vector and Inner_Product from Library
hoelzl [Fri, 30 Sep 2016 15:35:32 +0200] rev 63970
HOL-Analysis: move Continuum_Not_Denumerable from Library
hoelzl [Fri, 30 Sep 2016 12:00:17 +0200] rev 63969
HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
hoelzl [Fri, 30 Sep 2016 11:35:39 +0200] rev 63968
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)
paulson <lp15@cam.ac.uk> [Fri, 30 Sep 2016 14:05:51 +0100] rev 63967
new material on paths, etc. Also rationalisation
Manuel Eberl <eberlm@in.tum.de> [Fri, 30 Sep 2016 10:00:49 +0200] rev 63966
Merged
eberlm <eberlm@in.tum.de> [Thu, 29 Sep 2016 16:49:42 +0200] rev 63965
Set_Permutations replaced by more general Multiset_Permutations
boehmes [Thu, 29 Sep 2016 20:54:46 +0200] rev 63964
CONTRIBUTORS: new proof method "argo"