| Wed, 02 Aug 2006 22:26:47 +0200 |
wenzelm |
renamed thm_vars to thm_varnames;
|
file |
diff |
annotate
|
| Fri, 28 Jul 2006 18:37:25 +0200 |
paulson |
Checking for unsound proofs. Tidying.
|
file |
diff |
annotate
|
| Mon, 17 Jul 2006 18:42:38 +0200 |
wenzelm |
replaced butlast by Library.split_last;
|
file |
diff |
annotate
|
| Thu, 11 May 2006 19:19:31 +0200 |
wenzelm |
avoid raw equality on type thm;
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 04:01:25 +0100 |
mengj |
Proof reconstruction now only takes names of theorems as input.
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:34:55 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 18:29:11 +0100 |
paulson |
tidying
|
file |
diff |
annotate
|
| Tue, 17 Jan 2006 10:26:36 +0100 |
paulson |
improved SPASS support
|
file |
diff |
annotate
|
| Thu, 27 Oct 2005 18:25:33 +0200 |
paulson |
sorted lemma lists
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 17:57:21 +0200 |
paulson |
minor code tidyig
|
file |
diff |
annotate
|
| Thu, 06 Oct 2005 10:14:22 +0200 |
paulson |
major simplification: removal of the goalstring argument
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 09:59:01 +0200 |
paulson |
fixed the ascii-armouring of goalstring
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 12:45:16 +0200 |
paulson |
reduction in tracing files
|
file |
diff |
annotate
|
| Wed, 28 Sep 2005 11:16:27 +0200 |
paulson |
time limit option; fixed bug concerning first line of ATP output
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 14:09:48 +0200 |
paulson |
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 18:35:31 +0200 |
paulson |
improved proof parsing
|
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
|
| Thu, 15 Sep 2005 17:46:00 +0200 |
paulson |
massive tidy-up and simplification
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 17:47:37 +0200 |
paulson |
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
|
file |
diff |
annotate
|
| Thu, 08 Sep 2005 17:35:02 +0200 |
paulson |
consolidation of duplicate code in Isabelle-ATP linkup
|
file |
diff |
annotate
|
| Thu, 08 Sep 2005 13:24:19 +0200 |
paulson |
yet more tidying of Isabelle-ATP link
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 18:14:26 +0200 |
paulson |
Progress on eprover linkup, also massive tidying
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 21:29:33 +0200 |
quigley |
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 13:09:40 +0200 |
paulson |
nicer list of axioms used
|
file |
diff |
annotate
|
| Fri, 22 Jul 2005 17:43:03 +0200 |
paulson |
reformatting and tidying
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2005 20:26:31 +0200 |
quigley |
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
|
file |
diff |
annotate
|
| Tue, 21 Jun 2005 23:44:18 +0200 |
quigley |
Integrated vampire lemma code.
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 18:39:24 +0200 |
quigley |
Added VampCommunication.ML.
|
file |
diff |
annotate
|