#130 (Apr 4, 2016, 10:44:07 PM)

1. merged (detail / hgweb)
2. tuned -- more explicit sections; (detail / hgweb)
3. clarified bootstrap -- avoid conditional compilation in ROOT.ML; (detail / hgweb)
4. allow empty string; (detail / hgweb)
5. tuned; (detail / hgweb)
6. clarified modules; (detail / hgweb)
7. option ML_system_unsafe; (detail / hgweb)
8. clarified conditional compilation; (detail / hgweb)
9. clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity; (detail / hgweb)
10. clarified bootstrap -- more uniform use of ML files; (detail / hgweb)
11. clarified bootstrap; (detail / hgweb)
12. clarified final setup of ML environment; (detail / hgweb)
13. clarified modules; (detail / hgweb)
14. avoid duplicate reports; (detail / hgweb)

Started by an SCM change