src/Pure/library.ML
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;
2006-12-29 wenzelm 2006-12-29 added signed_string_of_int (pruduces proper - instead of SML's ~);
2006-12-28 wenzelm 2006-12-28 removed nospaces (Char.isSpace does not conform to Isabelle conventions);
2006-12-22 paulson 2006-12-22 string primtives
2006-12-15 wenzelm 2006-12-15 tuned -- accomodate Alice;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-11-23 wenzelm 2006-11-23 moved string_of_pair/list/option to structure ML_Syntax;
2006-11-16 wenzelm 2006-11-16 moved some fundamental concepts to General/basics.ML;
2006-11-13 haftmann 2006-11-13 added higher-order combinators for structured results
2006-11-05 wenzelm 2006-11-05 removed obsolete first_duplicate;
2006-10-31 haftmann 2006-10-31 cleanup
2006-10-11 haftmann 2006-10-11 abandoned findrep
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-07 wenzelm 2006-10-07 added the_single;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-12 wenzelm 2006-09-12 tuned eq_list;
2006-08-31 paulson 2006-08-31 Empty is better than Match
2006-08-08 haftmann 2006-08-08 abandoned equal_list in favor for eq_list
2006-07-17 webertj 2006-07-17 butlast removed (use fst o split_last instead)
2006-07-15 webertj 2006-07-15 function butlast added
2006-07-12 haftmann 2006-07-12 added chop_prefix
2006-07-11 wenzelm 2006-07-11 replaced read_radixint by read_intinf;
2006-07-04 wenzelm 2006-07-04 removed parrot comment;
2006-07-03 webertj 2006-07-03 comment added
2006-06-06 wenzelm 2006-06-06 added zip_options;
2006-05-20 wenzelm 2006-05-20 removed obsolete partition (cf. List.partition); tuned;
2006-05-16 wenzelm 2006-05-16 added divide_and_conquer combinator (by Amine Chaieb); removed remains of old option type; removed obsolete eq_opt; removed obsolete string_of_bool (use Bool.toString instead); tuned;
2006-05-09 haftmann 2006-05-09 removed superfluous eq_ord
2006-05-08 webertj 2006-05-08 string_of_option tuned
2006-05-05 webertj 2006-05-05 string_of_... functions added
2006-05-02 wenzelm 2006-05-02 sys_error: exception SYS_ERROR;
2006-04-30 wenzelm 2006-04-30 added serial_string;
2006-04-27 wenzelm 2006-04-27 renamed mapfilter to map_filter, made pervasive (again); made flat pervasive (again); added maps;
2006-04-26 wenzelm 2006-04-26 removed splitAt (superceded by chop); removed if_none (superceded by the_default);
2006-04-25 wenzelm 2006-04-25 made 'flat' pervasive (again);