src/Pure/library.ML
2012-08-23 ago prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
2012-07-16 ago replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
2012-04-16 ago redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
2012-03-21 ago prefer explicitly qualified exception List.Empty;
2012-03-19 ago discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
2012-03-19 ago moved some legacy stuff;
2012-03-12 ago some support for grouped list operations;
2012-03-08 ago tuned;
2012-03-03 ago discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
2011-11-24 ago more abstract datatype stamp, which avoids pointless allocation of mutable cells;
2011-09-01 ago more flexible sorting;
2011-07-13 ago low-level tuning;
2011-07-04 ago pervasive Basic_Library in Scala;
2011-06-30 ago getenv_strict in ML;
2011-06-27 ago old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-08 ago more robust exception pattern General.Subscript;
2011-04-19 ago slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
2011-01-12 ago smart_string_of_real: print integer values without fractional part;
2011-01-10 ago made SML/NJ happy;
2011-01-10 ago tuned string_of_int to avoid allocation for small integers;
2011-01-10 ago standardized split_last/last_elem towards List.last;
2010-12-03 ago removed confusing comments (cf. 500171e7aa59);
2010-12-03 ago really fixed comment (cf. 7abeb749ae99)
2010-12-03 ago fixing comment in library
2010-11-27 ago merged;
2010-11-26 ago strict forall2
2010-11-26 ago make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-26 ago just one version of fold_rev2;
2010-11-20 ago renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-16 ago added forall2 predicate lifter
2010-11-12 ago tuned signatures;
2010-11-03 ago discontinued obsolete function sys_error and exception SYS_ERROR;
2010-10-30 ago support for real valued configuration options;
2010-10-01 ago chop_while replace drop_while and take_while
2010-09-30 ago take_while, drop_while
2010-09-22 ago renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-07-20 ago tuned;
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-26 ago tuned white space;
2009-12-09 ago take and drop as projections of chop
2009-11-24 ago curried take/drop
2009-10-26 ago avoid upto if not needed
2009-10-23 ago merged
2009-10-22 ago restored accidentally deleted submultiset
2009-10-22 ago multiset operations with canonical argument order
2009-10-22 ago made SML/NJ happy;
2009-10-22 ago map_range (and map_index) combinator
2009-10-21 ago merged
2009-10-21 ago curried inter as canonical list operation (beware of argument order)
2009-10-21 ago merged
2009-10-21 ago curried union as canonical list operation
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-17 ago tuned/moved divide_and_conquer';
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-29 ago Raw ML references as unsynchronized state variables.
2009-08-10 ago added map_transpose
2009-07-25 ago eliminated redundant Library.multiply;
2009-07-10 ago dropped find_index_eq