src/Pure/search.ML
2014-01-30 blanchet 2014-01-30 systematically suppress tracing if asked for (affects 'meson' proof method)
2012-07-15 wenzelm 2012-07-15 prefer canonical fold_rev;
2012-02-15 wenzelm 2012-02-15 eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
2010-08-27 wenzelm 2010-08-27 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-11-02 wenzelm 2009-11-02 DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);
2009-10-29 wenzelm 2009-10-29 DEEPEN: less aggressive tracing, subject to trace_DEEPEN;
2009-10-15 wenzelm 2009-10-15 tuned signature; tuned;
2009-10-15 wenzelm 2009-10-15 renamed functor HeapFun to Heap;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2007-07-18 aspinall 2007-07-18 DEEPEN: Use priority message channel for interim messages (not warnings).
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-01-05 paulson 2007-01-05 Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever
2006-10-04 webertj 2006-10-04 tuned
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-02-03 wenzelm 2006-02-03 canonical member/insert/merge;
2005-06-02 wenzelm 2005-06-02 header;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2003-08-21 paulson 2003-08-21 Change from "tracing" to "warning", as requested by David Aspinall
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2000-07-23 wenzelm 2000-07-23 tuned ThmHeap;
2000-06-20 paulson 2000-06-20 now uses the heap data structure for BEST_FIRST
2000-01-28 oheimb 2000-01-28 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
1998-11-25 wenzelm 1998-11-25 replaced prs by writeln;
1998-10-23 oheimb 1998-10-23 added SOLVE tactical
1998-10-20 wenzelm 1998-10-20 QUIET_BREADTH_FIRST;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-04-02 paulson 1997-04-02 DEEPEN now takes an upper bound for terminating searches
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1996-11-01 paulson 1996-11-01 Replaced min by Int.min
1996-03-18 paulson 1996-03-18 New file containing search tacticals