src/Pure/library.ML
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';
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Tue, 29 Sep 2009 11:48:32 +0200 wenzelm Raw ML references as unsynchronized state variables.
Mon, 10 Aug 2009 12:24:47 +0200 haftmann added map_transpose
Sat, 25 Jul 2009 12:43:45 +0200 wenzelm eliminated redundant Library.multiply;
Fri, 10 Jul 2009 07:59:27 +0200 haftmann dropped find_index_eq
Sun, 24 May 2009 15:02:23 +0200 haftmann funpow_yield; tuned
Wed, 18 Mar 2009 20:03:01 +0100 wenzelm Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion;
Wed, 18 Mar 2009 15:23:52 +0100 haftmann made SML/NJ happy
Tue, 17 Mar 2009 14:09:20 +0100 wenzelm renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Fri, 13 Feb 2009 07:53:38 +1100 kleing New command find_consts searching for constants by type (by Timothy Bourke).
Thu, 11 Dec 2008 17:55:51 +0100 ballarin Clarified comment.
less more (0) -300 -100 -60 tip