#825 (Apr 4, 2017, 4:46:07 PM)

1. back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD"; (detail / hgweb)
2. tuned headers; (detail / hgweb)
3. proper imports;
   tuned headers; (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 4 sec waiting;
• 1 hr 34 min build duration;
• 1 hr 39 min total from scheduled to completion.