| Thu, 02 Sep 2010 11:29:02 +0200 |
blanchet |
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
|
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, 27 Jul 2009 23:17:40 +0200 |
wenzelm |
proper context for SAT tactics;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:57 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 15:50:45 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
file |
diff |
annotate
|
| Sun, 25 Sep 2005 01:12:49 +0200 |
webertj |
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
|
file |
diff |
annotate
|
| Sat, 24 Sep 2005 13:54:35 +0200 |
webertj |
cnf_struct renamed to cnf
|
file |
diff |
annotate
|
| Sat, 24 Sep 2005 13:11:05 +0200 |
obua |
preliminary fix of HOL build problem
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
file |
diff |
annotate
|