2007-07-18 ago DEEPEN: Use priority message channel for interim messages (not warnings).
2007-05-31 ago simplified/unified list fold;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-01-05 ago Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever
2006-10-04 ago tuned
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-02-03 ago canonical member/insert/merge;
2005-06-02 ago header;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2003-08-21 ago Change from "tracing" to "warning", as requested by David Aspinall
2001-11-21 ago use tracing function for trace output;
2000-07-23 ago tuned ThmHeap;
2000-06-20 ago now uses the heap data structure for BEST_FIRST
2000-01-28 ago added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
1998-11-25 ago replaced prs by writeln;
1998-10-23 ago added SOLVE tactical
1998-10-20 ago QUIET_BREADTH_FIRST;
1997-11-21 ago changed Sequence interface (now Seq, in seq.ML);
1997-07-22 ago Removal of the tactical STATE
1997-04-02 ago DEEPEN now takes an upper bound for terminating searches
1997-02-21 ago Replaced "flat" by the Basis Library function List.concat
1996-11-01 ago Replaced min by Int.min
1996-03-18 ago New file containing search tacticals