src/Pure/ML/ml_name_space.ML
2016-04-09 wenzelm 2016-04-09 shared output primitives of physical/virtual Pure;
2016-04-09 wenzelm 2016-04-09 shared thread position for physical/virtual Pure;
2016-04-09 wenzelm 2016-04-09 clarified bootstrap;
2016-04-07 wenzelm 2016-04-07 section headings for ROOT.ML;
2016-04-07 wenzelm 2016-04-07 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; handle bootstrap signatures as well;
2016-04-07 wenzelm 2016-04-07 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
2016-04-06 wenzelm 2016-04-06 clarified bootstrap;
2016-04-05 wenzelm 2016-04-05 clarified bootstrap environment;
2016-04-05 wenzelm 2016-04-05 tuned;
2016-04-04 wenzelm 2016-04-04 tuned;
2016-04-04 wenzelm 2016-04-04 tuned;
2016-04-04 wenzelm 2016-04-04 option ML_system_unsafe;
2016-04-03 wenzelm 2016-04-03 clarified SML name space: no access to structure PolyML;
2016-04-02 wenzelm 2016-04-02 careful export of type-dependent functions, without losing their special status;
2016-03-17 wenzelm 2016-03-17 hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
2016-03-17 wenzelm 2016-03-17 tuned signature;
2016-03-03 wenzelm 2016-03-03 obsolete;
2016-03-03 wenzelm 2016-03-03 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;