src/Pure/ML/ml_compiler0.ML
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-04-09 wenzelm 2016-04-09 clarified modules;
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-07 wenzelm 2016-04-07 simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
2016-04-07 wenzelm 2016-04-07 clarified bootstrap of @{make_string} -- avoid query on ML environment;
2016-04-06 wenzelm 2016-04-06 more robust bootstrap;
2016-04-06 wenzelm 2016-04-06 simplified bootstrap: critical structures remain accessible in ML_Root context;
2016-04-05 wenzelm 2016-04-05 avoid malformed Isabelle symbols during bootstrap;
2016-04-02 wenzelm 2016-04-02 tuned signature;
2016-04-02 wenzelm 2016-04-02 careful export of type-dependent functions, without losing their special status;
2016-04-02 wenzelm 2016-04-02 clarified modules;
2016-03-26 wenzelm 2016-03-26 explicit print_depth for the sake of Spec_Check.determine_type;
2016-03-18 wenzelm 2016-03-18 discontinued slightly odd "secure" mode;
2016-03-17 wenzelm 2016-03-17 @{make_string} is available during Pure bootstrap;
2016-03-06 wenzelm 2016-03-06 clarified treatment of fragments of Isabelle symbols during bootstrap;
2016-03-03 wenzelm 2016-03-03 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;