src/Pure/library.ML
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