| Tue, 20 Sep 2005 18:43:39 +0200 |
paulson |
tidying, and support for axclass/classrel clauses
|
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
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 09:54:31 +0200 |
paulson |
axioms now included in tptp files, no /bin/cat and various tidying
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 17:38:18 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 17:55:24 +0200 |
paulson |
further tidying up of Isabelle-ATP link
|
file |
diff |
annotate
|
| Fri, 26 Aug 2005 19:36:07 +0200 |
quigley |
DFG output now works for untyped rules (ML "ResClause.untyped();")
|
file |
diff |
annotate
|
| Fri, 29 Jul 2005 15:20:29 +0200 |
paulson |
nameless theorems: better names, flag to omit them
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 17:56:27 +0200 |
paulson |
invents theorem names; also patches write_out_clasimp
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 16:26:59 +0200 |
quigley |
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
|
file |
diff |
annotate
|
| Fri, 22 Jul 2005 17:43:49 +0200 |
paulson |
dead code removal
|
file |
diff |
annotate
|
| Wed, 20 Jul 2005 17:00:28 +0200 |
paulson |
code streamlining
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 15:06:04 +0200 |
paulson |
relevance filtering is now optional
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 18:25:02 +0200 |
paulson |
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
|
file |
diff |
annotate
|
| Fri, 10 Jun 2005 16:15:36 +0200 |
quigley |
All subgoals sent to the watcher at once now.
|
file |
diff |
annotate
|
| Wed, 01 Jun 2005 14:50:48 +0200 |
paulson |
small tweaks; also now write_out_clasimp takes the current theory as argument
|
file |
diff |
annotate
|
| Tue, 31 May 2005 12:42:36 +0200 |
quigley |
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
|
file |
diff |
annotate
|
| Tue, 24 May 2005 10:23:24 +0200 |
paulson |
A new structure and reduced indentation
|
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, 12 May 2005 18:24:42 +0200 |
paulson |
theorem names for caching
|
file |
diff |
annotate
|
| Tue, 03 May 2005 14:27:21 +0200 |
quigley |
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
|
file |
diff |
annotate
|
| Mon, 02 May 2005 13:30:48 +0200 |
paulson |
deleted redundant code
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:56:58 +0200 |
paulson |
fixed treatment of higher-order simprules
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 15:05:24 +0200 |
paulson |
added hearder lines and deleted some redundant material
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 18:01:50 +0200 |
quigley |
Corrected the problem with the ATP directory.
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 18:08:44 +0200 |
paulson |
more tidying of libraries in Reconstruction
|
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, 31 Mar 2005 19:47:30 +0200 |
quigley |
*** empty log message ***
|
file |
diff |
annotate
|