#620 (May 4, 2018, 12:50:11 AM)

1. Some tidying up (mostly regarding summations from 0) (detail / hgweb)
2. tidied up Infinite_Products (detail / hgweb)
3. merged (detail / hgweb)
4. fixed HOL-Analysis (detail / hgweb)
5. merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space) (detail / hgweb)
6. added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly (detail / hgweb)
7. a lemma about infinite products (detail / hgweb)
8. merged (detail / hgweb)
9. tidying up and using real induction methods (detail / hgweb)

Started by an SCM change

This run spent:

• 9.4 sec waiting;
• 1 hr 28 min build duration;
• 1 hr 28 min total from scheduled to completion.