| Mon, 23 Jan 2006 11:38:43 +0100 |
paulson |
Clausification now handles some IFs in rewrite rules (if-split did not work)
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:13 +0100 |
wenzelm |
Output.debug;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:12:58 +0100 |
wenzelm |
ProofContext.def_export;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 17:34:46 +0100 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 14 Dec 2005 16:14:26 +0100 |
paulson |
removal of some redundancies (e.g. one-point-rules) in clause production
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 15:27:43 +0100 |
paulson |
removal of functional reflexivity axioms
|
file |
diff |
annotate
|
| Fri, 18 Nov 2005 07:05:11 +0100 |
mengj |
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 15:29:23 +0100 |
paulson |
new version of "tryres" allowing multiple unifiers (apparently needed for
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 18:01:33 +0100 |
paulson |
Skolemization by inference, but not quite finished
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:27:51 +0200 |
wenzelm |
renamed Goal constant to prop;
|
file |
diff |
annotate
|
| Fri, 14 Oct 2005 15:34:56 +0200 |
paulson |
signature changes
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 12:44:25 +0200 |
paulson |
moved concat_with_and to watcher.ML
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 11:15:52 +0200 |
paulson |
the experimental tagging system, and the usual tidying
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:22 +0200 |
wenzelm |
tuned concat_with_and;
|
file |
diff |
annotate
|
| Tue, 28 Jun 2005 15:28:04 +0200 |
paulson |
stricter first-order check for meson
|
file |
diff |
annotate
|
| Fri, 24 Jun 2005 17:25:10 +0200 |
paulson |
meson method taking an argument list
|
file |
diff |
annotate
|
| Wed, 01 Jun 2005 18:19:59 +0200 |
paulson |
clausification bug fix
|
file |
diff |
annotate
|
| Fri, 20 May 2005 18:35:10 +0200 |
paulson |
bug fixes for clause form transformation
|
file |
diff |
annotate
|
| Wed, 18 May 2005 10:24:11 +0200 |
paulson |
new cnf function taking Skolemization theorems as an extra argument
|
file |
diff |
annotate
|
| Mon, 16 May 2005 10:29:15 +0200 |
paulson |
Use of IntInf.int instead of int in most numeric simprocs; avoids
|
file |
diff |
annotate
|
| Mon, 09 May 2005 16:40:37 +0200 |
paulson |
unfolding of Ex1
|
file |
diff |
annotate
|
| Mon, 02 May 2005 16:28:33 +0200 |
paulson |
meta-logic connectives now forbidden
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:56:58 +0200 |
paulson |
fixed treatment of higher-order simprules
|
file |
diff |
annotate
|
| Wed, 27 Apr 2005 16:40:27 +0200 |
paulson |
removed unnecessary (?) check
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 16:03:17 +0200 |
quigley |
Removed remaining references to Main.thy in reconstruction code.
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 15:15:06 +0200 |
quigley |
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
|
file |
diff |
annotate
|
| Fri, 15 Apr 2005 13:35:53 +0200 |
paulson |
more tidying up of the SPASS interface
|
file |
diff |
annotate
|
| Tue, 12 Apr 2005 11:08:25 +0200 |
paulson |
tweaks mainly to achieve sml/nj compatibility
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 18:20:04 +0200 |
quigley |
Integrating the reconstruction files into the building of HOL
|
file |
diff |
annotate
|
| Mon, 04 Apr 2005 18:43:18 +0200 |
quigley |
Updated to add watcher code.
|
file |
diff |
annotate
|
| Thu, 17 Mar 2005 15:12:03 +0100 |
paulson |
meson now checks that problems are first-order
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 18:40:36 +0100 |
paulson |
now checks for higher-order vars
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 16:55:36 +0100 |
paulson |
Tools/meson.ML: signature, structure and "open" rather than "local"
|
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
|
| 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
|