src/Pure/library.ML
2009-09-29 wenzelm 2009-09-29 Raw ML references as unsynchronized state variables.
2009-08-10 haftmann 2009-08-10 added map_transpose
2009-07-25 wenzelm 2009-07-25 eliminated redundant Library.multiply;
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-05-24 haftmann 2009-05-24 funpow_yield; tuned
2009-03-18 wenzelm 2009-03-18 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;
2009-03-18 haftmann 2009-03-18 made SML/NJ happy
2009-03-17 wenzelm 2009-03-17 renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-13 kleing 2009-02-13 New command find_consts searching for constants by type (by Timothy Bourke).
2008-12-11 ballarin 2008-12-11 Clarified comment.
2008-11-10 haftmann 2008-11-10 clarified comment
2008-10-09 haftmann 2008-10-09 removed legacy |>>>
2008-09-25 haftmann 2008-09-25 burrow_fst
2008-09-07 wenzelm 2008-09-07 added change_result;
2008-09-04 wenzelm 2008-09-04 Thread.getLocal/setLocal;
2008-08-27 wenzelm 2008-08-27 replaced find_substring by first_field;
2008-08-27 wenzelm 2008-08-27 added find_substring;
2008-08-13 wenzelm 2008-08-13 removed obsolete untabify (superceded by SymbolPos.tabify_content);
2008-03-27 haftmann 2008-03-27 changed wrong assignement in signature sections
2008-03-27 wenzelm 2008-03-27 tuned comments;
2008-02-16 wenzelm 2008-02-16 setmp: uninterruptible;
2008-01-26 wenzelm 2008-01-26 added surround;
2008-01-22 haftmann 2008-01-22 added map_split
2008-01-03 wenzelm 2008-01-03 added setmp_thread_data;
2008-01-01 wenzelm 2008-01-01 removed separate exists/forall code;
2007-12-18 wenzelm 2007-12-18 serial: now based on specific version in structure Multithreading;
2007-12-17 berghofe 2007-12-17 Added foldl1.
2007-12-05 wenzelm 2007-12-05 tuned signature;
2007-12-05 haftmann 2007-12-05 map_product and fold_product
2007-10-29 wenzelm 2007-10-29 added bool_ord;
2007-10-16 haftmann 2007-10-16 added yield_singleton
2007-10-16 wenzelm 2007-10-16 added perhaps_apply/loop;
2007-10-11 wenzelm 2007-10-11 removed obsolete flip;
2007-10-05 wenzelm 2007-10-05 added burrow_options;
2007-10-04 haftmann 2007-10-04 added nth_drop
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-09-16 wenzelm 2007-09-16 added some int constraints (ML_Parse.fix_ints not active here);
2007-08-03 wenzelm 2007-08-03 named some CRITICAL sections;
2007-07-29 wenzelm 2007-07-29 added list update;
2007-07-28 wenzelm 2007-07-28 setmp: NAMED_CRITICAL;
2007-07-24 wenzelm 2007-07-24 moved exception capture/release to structure Exn;
2007-07-23 wenzelm 2007-07-23 eliminated transform_failure (to avoid critical section for main transactions);
2007-07-23 wenzelm 2007-07-23 added setmp_noncritical; setmp: CRITICAL;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections (for multithreading);
2007-07-19 wenzelm 2007-07-19 added undefined: 'a -> 'b;
2007-07-17 wenzelm 2007-07-17 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
2007-07-10 wenzelm 2007-07-10 simplified funpow, untabify;
2007-06-19 wenzelm 2007-06-19 moved balanced tree operations to General/balanced_tree.ML;
2007-06-05 haftmann 2007-06-05 moved generic algebra modules
2007-06-03 wenzelm 2007-06-03 added flip (from General/basics.ML); renamed gen_submultiset to submultiset; moved downto0 to pattern.ML; moved legacy gen_merge_lists/merge_lists/merge_alists to Isar/locale.ML; moved plural to HOL/Tools/fundef_lib.ML; removed obsolete seq; simplified chop, fold2;
2007-06-02 krauss 2007-06-02 added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction
2007-04-04 paulson 2007-04-04 find_first is just an alias
2007-04-04 wenzelm 2007-04-04 removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);
2007-04-03 wenzelm 2007-04-03 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2007-02-28 wenzelm 2007-02-28 gensym: removed bits of dead code;
2007-02-27 paulson 2007-02-27 gensym no longer includes ' or _ in names (trailing _ is bad)
2007-02-07 berghofe 2007-02-07 Made untabify function tail recursive.
2007-01-21 nipkow 2007-01-21 Added lists-as-multisets functions
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;