#846 (Jan 18, 2019, 12:57:07 AM)

1. amending 689997a8a582 (detail / hgweb)
2. subsection is always %important (detail / hgweb)
3. no need for %unimportant for proofs of proposition (detail / hgweb)
4. redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7 (detail / hgweb)
5. revert to 56acd449da41 (detail / hgweb)
6. merge (detail / hgweb)
7. more tagging (detail / hgweb)
8. updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure (detail / hgweb)
9. chapters for analysis manual (detail / hgweb)

Started by an SCM change

This run spent:

• 7 min 5 sec waiting;
• 1 hr 18 min build duration;
• 1 hr 25 min total from scheduled to completion.