Summary
- 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