| Tue, 26 Oct 2010 12:17:19 +0200 |
blanchet |
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:57 +0200 |
haftmann |
moved sledgehammer to Plain; tuned dependencies
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 17:12:16 +0200 |
wenzelm |
just one refute.ML;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2009 12:14:12 +0100 |
blanchet |
added "no_assms" option to Refute, and include structured proof assumptions by default;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 11:46:13 +0100 |
blanchet |
avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy");
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:11:37 +0100 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Fri, 02 Oct 2009 21:41:57 +0200 |
wenzelm |
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 13:43:19 +0100 |
blanchet |
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:57 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Thu, 11 Jan 2007 01:34:23 +0100 |
webertj |
updated to mention the automatic unfolding of constants
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:43:09 +0100 |
haftmann |
moved upwars in HOL theory graph
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 15:50:44 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
file |
diff |
annotate
|
| Mon, 18 Jul 2005 15:49:34 +0200 |
webertj |
Documentation updated
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Wed, 17 Nov 2004 19:25:34 +0100 |
webertj |
removed explicit mentioning of zChaffs version number
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Wed, 26 May 2004 18:06:38 +0200 |
webertj |
documentation updated
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:17:37 +0200 |
wenzelm |
load ML files only once;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 13:51:04 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Thu, 11 Mar 2004 13:03:31 +0100 |
webertj |
Documentation updated
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 22:35:37 +0100 |
webertj |
*** empty log message ***
|
file |
diff |
annotate
|
| Sat, 10 Jan 2004 13:35:10 +0100 |
webertj |
Adding 'refute' to HOL.
|
file |
diff |
annotate
|