src/Pure/library.ML
2005-07-01 wenzelm 2005-07-01 low-level tuning of fold, fold_rev, foldl_map;
2005-06-22 wenzelm 2005-06-22 added structure Object (from Pure/General/object.ML);
2005-06-20 wenzelm 2005-06-20 added member, option_ord;
2005-06-17 wenzelm 2005-06-17 added serial numbers;
2005-06-02 wenzelm 2005-06-02 replaced foldl_string by fold_string; added forall_string; improved unsuffix/unprefix: no explode;
2005-05-31 wenzelm 2005-05-31 export filter; remove: generalized type;
2005-05-17 wenzelm 2005-05-17 removed rev_append; tuned presentation of datatype option: removed apsome, export the and if_none;
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-04-17 wenzelm 2005-04-17 clarified insert/remove; tuned canonical fold/fold_rev;
2005-04-16 wenzelm 2005-04-16 added gen_remove, remove; usual arrangement BasicLibrary: BASIC_LIBRARY and Library: LIBRARY;
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2005-04-07 wenzelm 2005-04-07 invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-10-26 berghofe 2004-10-26 Added function merge_alists'.
2004-07-19 berghofe 2004-07-19 Added function unprefix.
2004-07-16 wenzelm 2004-07-16 int_ord = Int.compare, string_ord = String.compare;
2004-07-11 wenzelm 2004-07-11 added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-18 wenzelm 2004-06-18 tuned exists_string;
2004-06-12 wenzelm 2004-06-12 added translate_string;
2004-06-05 wenzelm 2004-06-05 tuned exeption handling (capture/release);
2004-05-29 wenzelm 2004-05-29 output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
2004-05-21 berghofe 2004-05-21 - exported result datatype - added functions get_result and get_exn
2004-05-21 wenzelm 2004-05-21 added fold, product; removed transitive_closure;
2004-04-17 berghofe 2004-04-17 Fixed bug in rmod that caused an overflow exception in SML/NJ.
2004-03-19 paulson 2004-03-19 Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.
2003-07-11 berghofe 2003-07-11 Added several functions for producing random numbers.
2003-01-29 berghofe 2003-01-29 Added function rev_append.
2002-10-07 nipkow 2002-10-07 take/drop -> splitAt
2002-08-08 wenzelm 2002-08-08 transform_error: pass through Interrupt;
2002-02-20 wenzelm 2002-02-20 removed obscure functions bump_int_list, bump_list, bump_string;
2002-01-17 wenzelm 2002-01-17 added timeap_msg;
2001-12-08 wenzelm 2001-12-08 export writeln_default; tuned prefix_lines;
2001-12-03 wenzelm 2001-12-03 removed questionable init_gensym;
2001-11-26 wenzelm 2001-11-26 clarified order in gen_merge_lists';
2001-11-24 wenzelm 2001-11-24 added gen_merge_lists(') and merge_lists('); removed obsolete generic_extend, generic_merge, extend_list;
2001-11-21 wenzelm 2001-11-21 added tracing, tracing_fn;
2001-11-20 wenzelm 2001-11-20 added prefixes1, suffixes1;
2001-11-11 wenzelm 2001-11-11 added unflat;
2001-10-20 wenzelm 2001-10-20 conditional: bool -> (unit -> unit) -> unit; std_error: string -> unit;
2001-10-15 wenzelm 2001-10-15 map_nth_elem;
2001-08-31 berghofe 2001-08-31 Added function unique_strings.
2001-02-01 wenzelm 2001-02-01 comment
2001-01-30 oheimb 2001-01-30 added foldln
2001-01-21 wenzelm 2001-01-21 added replicate_string;
2000-12-18 nipkow 2000-12-18 added rational arithmetic
2000-09-04 wenzelm 2000-09-04 tuned;
2000-09-01 wenzelm 2000-09-01 added priority, priority_fn;
2000-08-29 nipkow 2000-08-29 *** empty log message ***
2000-06-25 wenzelm 2000-06-25 added change: 'a ref -> ('a -> 'a) -> unit;
2000-05-30 wenzelm 2000-05-30 global timing flag;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-03-13 wenzelm 2000-03-13 added |>> and |>>>;
1999-12-01 paulson 1999-12-01 fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER (for Moscow ML)
1999-10-05 wenzelm 1999-10-05 added untabify;
1999-09-04 wenzelm 1999-09-04 equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool;
1999-07-27 paulson 1999-07-27 added gen_inter
1999-07-10 wenzelm 1999-07-10 try/can: pass Interrupt and ERROR; nth_elem_string: use try;
1999-05-12 wenzelm 1999-05-12 strip_quotes replaced by unenclose;