src/Pure/library.ML
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
1994-01-19 wenzelm 1994-01-19 major cleanup and reorganisation; added generic_extend, generic_merge; added various minor functions;
1993-12-29 wenzelm 1993-12-29 added sys_error;
1993-11-30 wenzelm 1993-11-30 changed split_filename, remove_ext; added base_name;
1993-11-29 wenzelm 1993-11-29 added equal, not_equal: ''a -> ''a -> bool
1993-10-08 wenzelm 1993-10-08 added cons, rcons, last_elem, sort_strings, take_suffix; improved tack_on;
1993-10-05 clasohm 1993-10-05 added functions that operate on filenames: split_filename (originally located in Pure/read.ML), tack_on, remove_ext
1993-09-16 clasohm 1993-09-16 Initial revision