src/Pure/ML-Systems/ml_system.ML
2012-07-21 wenzelm 2012-07-21 more ML_System operations;
2011-07-23 wenzelm 2011-07-23 explicit structure ML_System; tunned ML bootstrap;