src/Pure/search.ML
Fri, 27 Aug 2010 16:29:12 +0200 wenzelm clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Mon, 02 Nov 2009 17:30:38 +0100 wenzelm DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);
Thu, 29 Oct 2009 20:35:47 +0100 wenzelm DEEPEN: less aggressive tracing, subject to trace_DEEPEN;
Thu, 15 Oct 2009 11:23:03 +0200 wenzelm tuned signature;
Thu, 15 Oct 2009 11:12:09 +0200 wenzelm renamed functor HeapFun to Heap;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Wed, 18 Jul 2007 14:46:59 +0200 aspinall DEEPEN: Use priority message channel for interim messages (not warnings).
Thu, 31 May 2007 23:47:36 +0200 wenzelm simplified/unified list fold;
Mon, 26 Feb 2007 23:18:24 +0100 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
Fri, 05 Jan 2007 17:38:05 +0100 paulson Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever
Wed, 04 Oct 2006 11:50:37 +0200 webertj tuned
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Fri, 03 Feb 2006 23:12:28 +0100 wenzelm canonical member/insert/merge;
Thu, 02 Jun 2005 09:11:32 +0200 wenzelm header;
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Thu, 21 Aug 2003 11:41:44 +0200 paulson Change from "tracing" to "warning", as requested by David Aspinall
Wed, 21 Nov 2001 00:36:51 +0100 wenzelm use tracing function for trace output;
Sun, 23 Jul 2000 12:04:56 +0200 wenzelm tuned ThmHeap;
Tue, 20 Jun 2000 11:54:07 +0200 paulson now uses the heap data structure for BEST_FIRST
Fri, 28 Jan 2000 11:23:41 +0100 oheimb added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
Wed, 25 Nov 1998 13:57:44 +0100 wenzelm replaced prs by writeln;
Fri, 23 Oct 1998 20:34:59 +0200 oheimb added SOLVE tactical
Tue, 20 Oct 1998 16:33:47 +0200 wenzelm QUIET_BREADTH_FIRST;
Fri, 21 Nov 1997 15:27:43 +0100 wenzelm changed Sequence interface (now Seq, in seq.ML);
Tue, 22 Jul 1997 11:14:18 +0200 paulson Removal of the tactical STATE
Wed, 02 Apr 1997 15:24:42 +0200 paulson DEEPEN now takes an upper bound for terminating searches
Fri, 21 Feb 1997 15:31:47 +0100 paulson Replaced "flat" by the Basis Library function List.concat
Fri, 01 Nov 1996 15:15:39 +0100 paulson Replaced min by Int.min
Mon, 18 Mar 1996 13:42:35 +0100 paulson New file containing search tacticals
less more (0) tip