| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 20:53:40 +0200 |
wenzelm |
removed some unreferenced material;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Fri, 16 Oct 2009 10:45:10 +0200 |
wenzelm |
local channels for tracing/debugging;
|
file |
diff |
annotate
|
| 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
|
| Mon, 12 Nov 2007 20:10:34 +0100 |
wenzelm |
changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 17:34:27 +0200 |
paulson |
Improving the propagation of type constraints for Frees
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 15:59:31 +0200 |
paulson |
rationalized redundant code
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 10:23:09 +0200 |
paulson |
failure messages
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 18:14:00 +0200 |
paulson |
context-based treatment of generalization; also handling TFrees in axiom clauses
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 22:23:27 +0200 |
wenzelm |
TypeInfer.constrain: canonical argument order;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 17:53:37 +0200 |
paulson |
metis now available in PreList
|
file |
diff |
annotate
|
| Fri, 07 Sep 2007 15:35:25 +0200 |
paulson |
allow TVars during type inference
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 17:03:53 +0200 |
paulson |
Vampire structured proofs. Better parsing; some bug fixes.
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 22:35:34 +0200 |
wenzelm |
replaced ProofContext.infer_types by general Syntax.check_terms;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:16:44 +0200 |
paulson |
Returning both a "one-line" proof and a structured proof
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 18:30:11 +0200 |
paulson |
Modified message for sendback
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 13:59:46 +0200 |
paulson |
Fixing the code to undo the function ascii_of
|
file |
diff |
annotate
|
| Tue, 17 Jul 2007 16:06:13 +0200 |
paulson |
Full sort information by default.
|
file |
diff |
annotate
|
| Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
file |
diff |
annotate
|
| Thu, 31 May 2007 01:25:24 +0200 |
wenzelm |
TextIO.inputLine: use present SML B library version;
|
file |
diff |
annotate
|
| Wed, 23 May 2007 14:52:12 +0200 |
paulson |
formatting
|
file |
diff |
annotate
|
| Thu, 19 Apr 2007 18:23:11 +0200 |
paulson |
trying to make single-step proofs work better, especially if they contain
|
file |
diff |
annotate
|
| Wed, 18 Apr 2007 21:30:14 +0200 |
wenzelm |
simplified ProofContext.infer_types(_pats);
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:49 +0200 |
wenzelm |
proper ProofContext.infer_types;
|
file |
diff |
annotate
|
| Thu, 29 Mar 2007 11:12:03 +0200 |
paulson |
Now checks for types-only clause before outputting.
|
file |
diff |
annotate
|
| Wed, 21 Mar 2007 13:58:36 +0100 |
paulson |
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
|
file |
diff |
annotate
|
| Mon, 19 Mar 2007 15:57:20 +0100 |
paulson |
No label on "show"; tries to remove dependencies more cleanly
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 13:10:22 +0100 |
paulson |
First stab at reconstructing HO problems
|
file |
diff |
annotate
|