Changes

Summary

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