| Fri, 06 Oct 2006 11:17:53 +0200 |
paulson |
renamed the combinator laws
|
file |
diff |
annotate
|
| Thu, 05 Oct 2006 10:41:27 +0200 |
paulson |
facts about combinators
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 18:29:26 +0200 |
wenzelm |
moved theory Infinite_Set to Library;
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 14:29:52 +0200 |
mengj |
Reordered how files are loaded.
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 16:01:34 +0200 |
paulson |
addition of combinators
|
file |
diff |
annotate
|
| Sun, 04 Jun 2006 10:50:41 +0200 |
mengj |
Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 05:46:39 +0100 |
mengj |
Added new file Tools/ATP/reduce_axiomsN.ML
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 12:06:08 +0100 |
paulson |
new hash table module in HOL/Too/s
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 02:30:12 +0200 |
mengj |
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
|
file |
diff |
annotate
|
| Fri, 14 Oct 2005 11:36:14 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 15:35:29 +0200 |
paulson |
small tidy-up of utility functions
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 16:05:10 +0200 |
webertj |
spaces inserted in header
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:03:37 +0200 |
wenzelm |
tuned theory dependencies;
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 18:30:22 +0200 |
paulson |
further simplification of the Isabelle-ATP linkup
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 15:12:13 +0200 |
paulson |
simplification of the Isabelle-ATP code; hooks for batch generation of problems
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:22 +0200 |
wenzelm |
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:45:17 +0200 |
paulson |
moving Commutative_Ring to the correct theory
|
file |
diff |
annotate
|
| Thu, 08 Sep 2005 17:35:02 +0200 |
paulson |
consolidation of duplicate code in Isabelle-ATP linkup
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 18:22:29 +0200 |
paulson |
elimination of watcher.sig
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 21:29:55 +0200 |
quigley |
Added ECommunication.ML
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 15:24:58 +0200 |
paulson |
deleted obsolete VampireCommunication.ML
|
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
|
| Mon, 20 Jun 2005 21:33:27 +0200 |
wenzelm |
use Tools/ATP/VampCommunication.ML;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 26 May 2005 16:50:20 +0200 |
paulson |
goodby to modUnix
|
file |
diff |
annotate
|
| Mon, 23 May 2005 00:18:51 +0200 |
quigley |
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
|
file |
diff |
annotate
|
| Thu, 19 May 2005 11:08:15 +0200 |
paulson |
Skolemization of simprules and classical rules
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:56:58 +0200 |
paulson |
fixed treatment of higher-order simprules
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 18:08:44 +0200 |
paulson |
more tidying of libraries in Reconstruction
|
file |
diff |
annotate
|
| Tue, 12 Apr 2005 11:08:25 +0200 |
paulson |
tweaks mainly to achieve sml/nj compatibility
|
file |
diff |
annotate
|
| Fri, 08 Apr 2005 18:43:39 +0200 |
paulson |
Reconstruction code, now packaged to avoid name clashes
|
file |
diff |
annotate
|
| Fri, 08 Apr 2005 10:50:02 +0200 |
paulson |
temporarily removed ATP code
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 17:45:51 +0200 |
quigley |
Reconstruction.thy and IsaMakefile updated
|
file |
diff |
annotate
|
| Mon, 04 Apr 2005 18:43:18 +0200 |
quigley |
Updated to add watcher code.
|
file |
diff |
annotate
|
| Fri, 01 Apr 2005 11:12:39 +0200 |
paulson |
patch to get it working again
|
file |
diff |
annotate
|
| Tue, 07 Dec 2004 16:16:10 +0100 |
paulson |
all theories must be related to Reconstruction
|
file |
diff |
annotate
|
| Thu, 02 Dec 2004 11:09:19 +0100 |
paulson |
new CLAUSIFY attribute for proof reconstruction with lemmas
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:21:03 +0200 |
paulson |
proof reconstruction for external ATPs
|
file |
diff |
annotate
|