2010-11-27 ago removed bash from ML system bootstrap, and past the Secure ML barrier;
2010-11-20 ago renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-06 ago somewhat more uniform timing in ML vs. Scala;
2010-09-22 ago renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-22 ago main Isabelle_Process via Isabelle_System.Managed_Process;
2010-05-12 ago conditional structure SingleAssignment;
2010-04-16 ago added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
2010-02-06 ago explicit representation of single-assignment variables;
2010-02-06 ago renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2009-12-19 ago added basic library -- Scala version;
2009-10-26 ago forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;
2009-10-22 ago support single-assigment variables -- based on magic RTS operations by David Matthews;
2009-10-19 ago always qualify NJ's old List.foldl/foldr in Isabelle/ML;
2009-09-30 ago more uniform treatment of structure Unsynchronized in ML bootstrap phase;
2009-09-29 ago hide "ref" by default, to enforce excplicit indication as Unsynchronized;
2009-09-29 ago Raw ML references as unsynchronized state variables.
2009-06-17 ago more detailed start_timing/end_timing (in timing.ML);
2009-06-01 ago removed print function from global ML name space, to reduce risk of surprises;
2009-05-31 ago no longer open PolyML -- to avoid surprises within the global name space;
2009-05-31 ago discontinued support for Poly/ML 4.x versions;
2009-03-23 ago more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-21 ago replaced install_pp/make_pp by more general toplevel_pp based on use_text;
2009-03-21 ago added generic ML_Pretty interface;
2009-03-01 ago end_timing: generalized result -- message plus with explicit time values;
2009-01-19 ago removed Ids;
2008-10-09 ago extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
2008-10-03 ago removed obsolete Posix/Signal compatibility wrappers;
2008-10-01 ago more robust treatment of Interrupt (cf. exn.ML);
2008-09-29 ago added type pp, which helps installing polymorphic pretty printers;
2008-09-17 ago use_text/use_file now depend on explicit ML name space;
2008-09-07 ago explicit use of universal.ML and dummy_thread.ML;
2008-03-28 ago added forget_structure;
2008-03-24 ago removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
2008-03-06 ago common setup for system_out/system;
2008-03-06 ago rearrangements to make latest Poly/ML the default, not old 4.x;