src/Pure/library.ML
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;
1997-11-03 wenzelm 1997-11-03 added distinct_fst_string;
1997-11-01 paulson 1997-11-01 Faster lexing
1997-10-30 wenzelm 1997-10-30 added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;
1997-10-23 wenzelm 1997-10-23 added sort_wrt;
1997-10-15 wenzelm 1997-10-15 tuned comment;
1997-10-10 wenzelm 1997-10-10 fixed space_explode, old one retained as BAD_space_explode; added split_lines;
1997-10-01 wenzelm 1997-10-01 added split_last;
1997-09-23 wenzelm 1997-09-23 added handle_error: ('a -> 'b) -> 'a -> 'b error;
1997-08-08 wenzelm 1997-08-08 added append_file;
1997-08-06 wenzelm 1997-08-06 added read_file, write_file;
1997-08-06 berghofe 1997-08-06 Added function "file_exists".
1997-07-22 wenzelm 1997-07-22 added error_msg;
1997-07-18 wenzelm 1997-07-18 improved output channels: normal, warning, error;
1997-06-05 paulson 1997-06-05 Removal of radixstring from string_of_int; addition of string_of_indexname
1997-06-03 wenzelm 1997-06-03 is_blank: fixed space2;
1997-05-30 paulson 1997-05-30 flushOut ensures that no recent error message are lost (not certain this is necessary)
1997-05-20 paulson 1997-05-20 Declares Option_ as synonym for structure Option
1997-04-29 wenzelm 1997-04-29 is_blank: added space2 (160);
1997-04-17 wenzelm 1997-04-17 renamed set_ap to setmp;
1997-04-16 wenzelm 1997-04-16 improved inc, dec; added set_ap;
1997-03-18 paulson 1997-03-18 gensym no longer generates random identifiers, but just enumerates them starting from A. The random number generator was needlessly slow and caused portability problems.
1997-01-17 wenzelm 1997-01-17 added gen_overwrite;
1997-01-13 wenzelm 1997-01-13 added datatype order;
1997-01-06 wenzelm 1997-01-06 added stamp util;
1996-12-16 wenzelm 1996-12-16 fixed comment;
1996-12-05 wenzelm 1996-12-05 added pwd;
1996-12-03 paulson 1996-12-03 Random number generated "downgraded" to generate numbers below 2^29 - 1, for MLWorks compatibility
1996-11-28 paulson 1996-11-28 Declares List_ as a synonym for List
1996-11-27 paulson 1996-11-27 Eta-expanded some declarations that are illegal under value polymorphism Converted I/O operatios for Basis Library compatibility
1996-11-18 wenzelm 1996-11-18 added is_printable: string -> bool;
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-12 paulson 1996-11-12 Updated syntax; shortened comments; put in monomorphic versions of ins
1996-11-04 paulson 1996-11-04 Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min
1996-09-25 paulson 1996-09-25 Prevention of Overflow exception (for SML/NJ) in gensym
1996-09-23 paulson 1996-09-23 Addition of gensym
1996-03-28 berghofe 1996-03-28 Added functions pr_latex and printgoal_latex which display current proof state in xdvi window
1996-03-20 paulson 1996-03-20 maketest now closes the output file Declared type mtree for proof objects
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-03-14 berghofe 1996-03-14 Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1996-01-29 clasohm 1996-01-29 added absolute_path
1995-12-18 clasohm 1995-12-18 added subdir_of
1995-11-23 clasohm 1995-11-23 files now define a structure to allow SML/NJ to optimize the code
1995-10-24 clasohm 1995-10-24 added space_explode and relative_path
1995-03-15 lcp 1995-03-15 Declares the function exit_use to behave like use but fail if errors are detected. It can be used in all Makefiles except Pure, which will write the exception handler explicitly ("exit" will have been declared already).
1994-08-18 lcp 1994-08-18 Pure/library/assert_all: new, moved from ZF/ind_syntax.ML
1994-08-12 lcp 1994-08-12 Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents Pure/library/is_blank: now handles form feeds () too, in accordance with ML definition
1994-06-01 wenzelm 1994-06-01 replaced infix also by |>
1994-05-19 wenzelm 1994-05-19 added infix op also: 'a * ('a -> 'b) -> 'b; added set, reset, toggle: bool ref -> bool; added find_first, exists2, forall2, commas_quote, merge_rev_lists;
1994-02-08 wenzelm 1994-02-08 added eq_set;
1994-02-03 wenzelm 1994-02-03 added if_none, parents, commas, gen_duplicates, duplicates, assoc2; changed cat_lines: no final "\n";
1994-01-20 nipkow 1994-01-20 removed square and fact