| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2009 02:07:06 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 14:09:59 +0200 |
boehmes |
Mirabelle: added preliminary documentation,
|
file |
diff |
annotate
|
| Sat, 29 Aug 2009 21:57:06 +0200 |
boehmes |
propagate theorem names, in addition to generated return message
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 18:17:36 +0200 |
wenzelm |
ResAxioms.neg_conjecture_clauses: proper context;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 11:21:02 +0200 |
immler |
check for correct proof output
|
file |
diff |
annotate
|
| Sun, 28 Jun 2009 15:01:29 +0200 |
immler |
check if conjectures have been used in proof
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 21:46:36 +0200 |
wenzelm |
ML_Compiler.exn_message;
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 16:56:41 +0200 |
immler |
include chain-ths in every prover-call
|
file |
diff |
annotate
|
| Mon, 04 May 2009 23:44:11 +0200 |
immler |
tuned
|
file |
diff |
annotate
|
| Mon, 04 May 2009 23:37:39 +0200 |
immler |
added Philipp Meyer's implementation of AtpMinimal
|
file |
diff |
annotate
|
| Sat, 04 Apr 2009 20:22:39 +0200 |
immler |
reverted to explicitly check the presence of a refutation
|
file |
diff |
annotate
|
| Thu, 02 Apr 2009 16:18:19 +0200 |
nipkow |
Updated to corrected E output messages
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 14:57:33 +0100 |
immler |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Jan 2009 16:05:57 +0100 |
immler |
modified remote script;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:17 +0100 |
wenzelm |
use regular Term.add_XXX etc.;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:14 +0100 |
wenzelm |
use exists_subterm directly;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2008 14:04:29 +0200 |
wenzelm |
** Update from Fabian **
|
file |
diff |
annotate
|
| Fri, 03 Oct 2008 16:37:09 +0200 |
wenzelm |
version of sledgehammer using threads instead of processes, misc cleanup;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 18:10:23 +0100 |
paulson |
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
|
file |
diff |
annotate
|
| Mon, 28 Jan 2008 22:27:19 +0100 |
wenzelm |
added ::: / @@@ scanner combinators;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 23:10:17 +0100 |
wenzelm |
removed strange MacRoman character;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 17:40:48 +0100 |
paulson |
Replaced refs by config params; finer critical section in mets method
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 16:26:03 +0100 |
paulson |
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
|
file |
diff |
annotate
|
| Mon, 12 Nov 2007 21:09:32 +0100 |
wenzelm |
back to sigusr2, after Poly/ML 5.1 has been adapted;
|
file |
diff |
annotate
|