src/Pure/library.ML
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;
1997-12-02 wenzelm 1997-12-02 added prod_ord, dict_ord, list_ord;
1997-11-28 paulson 1997-11-28 New timing functions startTiming and endTiming
1997-11-26 wenzelm 1997-11-26 removed merge_opts;
1997-11-20 wenzelm 1997-11-20 added type object = exn;
1997-11-20 wenzelm 1997-11-20 added get_error: 'a error -> string option, get_ok: 'a error -> 'a option; added multiply: 'a list * 'a list list -> 'a list list;
1997-11-13 wenzelm 1997-11-13 made SML/NJ happy;
1997-11-12 wenzelm 1997-11-12 major cleanup; removed several obsolete functions; moved file stuff to Thy/file.ML;
1997-11-10 oheimb 1997-11-10 polished definition of find_index_eq
1997-11-07 oheimb 1997-11-07 changed libraray function find to find_index_eq, currying it
1997-11-06 wenzelm 1997-11-06 tuned;
1997-11-05 wenzelm 1997-11-05 fixed exception OPTION; added try, can;