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