src/Pure/ROOT1.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 ML bootstrap;