src/Pure/library.ML
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;
1999-04-27 wenzelm 1999-04-27 added oooo;
1999-03-09 wenzelm 1999-03-09 added nth_elem_string, exists_string;
1999-02-13 wenzelm 1999-02-13 foldl_string;
1998-11-25 wenzelm 1998-11-25 removed prs / prs_fn (broken, because it did not include \n in its semantics, forcing writeln to add one uncoditionally); replaced prs_fn by writeln fn;
1998-11-24 wenzelm 1998-11-24 fixed prefix_lines: *separate* by \n;
1998-11-21 wenzelm 1998-11-21 std_output, prefix_lines;
1998-11-17 wenzelm 1998-11-17 val apply: ('a -> 'a) list -> 'a -> 'a; val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b;
1998-11-16 wenzelm 1998-11-16 added oo, ooo (*concatenation: 2 and 3 args*);
1998-08-10 wenzelm 1998-08-10 val single: 'a -> 'a list; val suffix: string -> string -> string; val unsuffix: string -> string -> string;
1998-07-02 wenzelm 1998-07-02 Symbol.beginning;
1998-06-15 wenzelm 1998-06-15 handle_error: capture error msgs, even if no exception raised;
1998-06-05 wenzelm 1998-06-05 removed type object (see object.ML);
1998-05-25 wenzelm 1998-05-25 added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list; added seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit; tuned 'beginning';
1998-05-19 wenzelm 1998-05-19 fixed handle_error: cat_lines;
1998-05-13 wenzelm 1998-05-13 added transform_error, exception ERROR_MESSAGE;
1998-05-13 wenzelm 1998-05-13 get_first: ('a -> 'b option) -> 'a list -> 'b option;
1998-05-04 wenzelm 1998-05-04 added nth_update: 'a -> int * 'a list -> 'a list;
1998-04-29 wenzelm 1998-04-29 tuned error msgs;
1998-04-04 wenzelm 1998-04-04 type_error;
1998-03-10 nipkow 1998-03-10 New simplifier flag for mutual simplification.
1998-03-09 wenzelm 1998-03-09 added merge_alists; moced is_letter etc. to Syntax/symbol.ML;
1998-02-18 wenzelm 1998-02-18 tuned comment;
1998-02-13 wenzelm 1998-02-13 added append (curried);
1998-02-12 wenzelm 1998-02-12 added explicit signature; improved comments;
1998-02-12 wenzelm 1998-02-12 improved is_letter etc.;
1997-12-29 wenzelm 1997-12-29 removed distinct_fst_string;
1997-12-24 wenzelm 1997-12-24 improved comment;
1997-12-19 wenzelm 1997-12-19 added rev_order, make_ord; reimplemented sort function: stable version of quicksort;
1997-12-04 wenzelm 1997-12-04 added eq_set;