Summary
- merged
- tuned -- more explicit sections;
- clarified bootstrap -- avoid conditional compilation in ROOT.ML;
- allow empty string;
- tuned;
- clarified modules;
- option ML_system_unsafe;
- clarified conditional compilation;
- clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
- clarified bootstrap -- more uniform use of ML files;
- clarified bootstrap;
- clarified final setup of ML environment;
- clarified modules;
- avoid duplicate reports;