src/Pure/library.ML
Fri, 31 May 2013 09:30:32 +0200 haftmann combinator fold_range, corresponding to map_range
Tue, 14 May 2013 20:46:09 +0200 wenzelm more uniform Markup.print_real;
Thu, 07 Mar 2013 15:02:55 +0100 wenzelm tuned signature -- prefer terminology of Scala and Axiom;
Wed, 16 Jan 2013 20:40:50 +0100 wenzelm eliminated dead code;
Sun, 30 Dec 2012 16:33:05 +0100 wenzelm tuned whitespace;
Thu, 23 Aug 2012 13:03:29 +0200 wenzelm prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
Mon, 16 Jul 2012 15:57:21 +0200 wenzelm replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
Mon, 16 Apr 2012 23:07:40 +0200 wenzelm 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;
Wed, 21 Mar 2012 11:00:34 +0100 wenzelm prefer explicitly qualified exception List.Empty;
Mon, 19 Mar 2012 21:16:19 +0100 wenzelm discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
Mon, 19 Mar 2012 21:10:33 +0100 wenzelm moved some legacy stuff;
Mon, 12 Mar 2012 23:16:02 +0100 wenzelm some support for grouped list operations;
Thu, 08 Mar 2012 21:35:54 +0100 wenzelm tuned;
Sat, 03 Mar 2012 22:27:30 +0100 wenzelm discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
Thu, 24 Nov 2011 21:15:20 +0100 wenzelm more abstract datatype stamp, which avoids pointless allocation of mutable cells;
Thu, 01 Sep 2011 14:10:52 +0200 wenzelm more flexible sorting;
Wed, 13 Jul 2011 20:13:27 +0200 wenzelm low-level tuning;
Mon, 04 Jul 2011 16:51:45 +0200 wenzelm pervasive Basic_Library in Scala;
Thu, 30 Jun 2011 13:59:55 +0200 wenzelm getenv_strict in ML;
Mon, 27 Jun 2011 15:03:55 +0200 wenzelm old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Tue, 19 Apr 2011 15:58:05 +0200 wenzelm slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
Wed, 12 Jan 2011 14:07:29 +0100 wenzelm smart_string_of_real: print integer values without fractional part;
Mon, 10 Jan 2011 16:56:47 +0100 wenzelm made SML/NJ happy;
Mon, 10 Jan 2011 16:07:16 +0100 wenzelm tuned string_of_int to avoid allocation for small integers;
Mon, 10 Jan 2011 15:19:48 +0100 wenzelm standardized split_last/last_elem towards List.last;
Fri, 03 Dec 2010 17:29:27 +0100 wenzelm removed confusing comments (cf. 500171e7aa59);
Fri, 03 Dec 2010 10:17:55 +0100 krauss really fixed comment (cf. 7abeb749ae99)
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn fixing comment in library
Sat, 27 Nov 2010 00:00:54 +0100 wenzelm merged;
Fri, 26 Nov 2010 23:13:58 +0100 haftmann strict forall2
Fri, 26 Nov 2010 22:29:41 +0100 wenzelm make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
Fri, 26 Nov 2010 22:04:33 +0100 wenzelm just one version of fold_rev2;
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Tue, 16 Nov 2010 10:33:36 +0100 haftmann added forall2 predicate lifter
Fri, 12 Nov 2010 14:51:28 +0100 wenzelm tuned signatures;
Wed, 03 Nov 2010 11:33:51 +0100 wenzelm discontinued obsolete function sys_error and exception SYS_ERROR;
Sat, 30 Oct 2010 16:33:58 +0200 wenzelm support for real valued configuration options;
Fri, 01 Oct 2010 10:25:36 +0200 haftmann chop_while replace drop_while and take_while
Thu, 30 Sep 2010 18:37:29 +0200 haftmann take_while, drop_while
Wed, 22 Sep 2010 18:21:48 +0200 wenzelm renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Tue, 20 Jul 2010 14:41:13 +0200 wenzelm tuned;
Wed, 05 May 2010 18:25:34 +0200 haftmann 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 =)
Fri, 26 Mar 2010 20:30:05 +0100 wenzelm tuned white space;
Wed, 09 Dec 2009 21:38:12 +0100 haftmann take and drop as projections of chop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Mon, 26 Oct 2009 15:16:28 +0100 haftmann avoid upto if not needed
Fri, 23 Oct 2009 10:11:56 +0200 haftmann merged
Thu, 22 Oct 2009 16:58:22 +0200 haftmann restored accidentally deleted submultiset
Thu, 22 Oct 2009 16:52:06 +0200 haftmann multiset operations with canonical argument order
Thu, 22 Oct 2009 17:54:47 +0200 wenzelm made SML/NJ happy;
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Wed, 21 Oct 2009 12:12:21 +0200 haftmann merged
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 12:08:52 +0200 haftmann merged
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Sat, 17 Oct 2009 22:34:19 +0200 wenzelm tuned/moved divide_and_conquer';
less more (0) -300 -100 -60 tip