| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Fri, 21 Jan 2005 13:52:57 +0100 |
paulson |
negate_nead (???) changed to negated_asm_of_head
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:21:03 +0200 |
paulson |
proof reconstruction for external ATPs
|
file |
diff |
annotate
|
| Fri, 06 Aug 2004 13:36:04 +0200 |
paulson |
make_clauses now meta
|
file |
diff |
annotate
|
| Sun, 11 Jul 2004 20:33:22 +0200 |
wenzelm |
local_cla/simpset_of;
|
file |
diff |
annotate
|
| Mon, 28 Jun 2004 11:15:13 +0200 |
paulson |
new method for explicit classical resolution
|
file |
diff |
annotate
|
| Wed, 09 Jun 2004 11:19:23 +0200 |
paulson |
fixed the skolemize method
|
file |
diff |
annotate
|
| Fri, 28 May 2004 11:20:04 +0200 |
paulson |
new skolemize_tac and skolemize method
|
file |
diff |
annotate
|
| Wed, 19 May 2004 11:31:26 +0200 |
paulson |
has_consts now handles the @-operator
|
file |
diff |
annotate
|
| Fri, 14 May 2004 16:49:12 +0200 |
paulson |
clauses for ordinary resolution
|
file |
diff |
annotate
|
| Tue, 11 May 2004 10:48:00 +0200 |
paulson |
conversion to clauses for ordinary resolution rather than ME
|
file |
diff |
annotate
|
| Tue, 07 May 2002 14:26:32 +0200 |
wenzelm |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2001 18:34:17 +0100 |
wenzelm |
moved lemmas to theory Hilbert_Choice;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:41:56 +0100 |
wenzelm |
CHANGED_PROP;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 21:06:01 +0200 |
wenzelm |
improved meson setup;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 10:15:23 +0200 |
paulson |
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
|
file |
diff |
annotate
|