src/Pure/ML/ml_pervasive1.ML
2016-04-06 wenzelm 2016-04-06 simplified bootstrap: critical structures remain accessible in ML_Root context;
2016-04-06 wenzelm 2016-04-06 clarified bootstrap;
2016-04-06 wenzelm 2016-04-06 clarified ML bootstrap;