| #
bc78ac03 |
|
29-Sep-2016 |
boehmes <none@none> |
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
42a54449 |
|
01-Feb-2014 |
wenzelm <none@none> |
more standard file/module names;
--HG--
rename : src/HOL/Tools/cnf_funcs.ML => src/HOL/Tools/cnf.ML
rename : src/HOL/Tools/sat_funcs.ML => src/HOL/Tools/sat.ML
|
| #
9eff77bb |
|
31-Oct-2012 |
blanchet <none@none> |
moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
|
| #
36418877 |
|
31-Oct-2012 |
blanchet <none@none> |
moved Refute to "HOL/Library" to speed up building "Main" even more
--HG--
rename : src/HOL/Refute.thy => src/HOL/Library/Refute.thy
rename : src/HOL/Tools/refute.ML => src/HOL/Library/refute.ML
|
| #
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
| #
1a8c5d7b |
|
03-Jan-2012 |
blanchet <none@none> |
tuned Refute
|
| #
2bc6dfb5 |
|
02-Sep-2010 |
blanchet <none@none> |
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
this *really* speeds up things -- HOL now builds 12% faster on my machine
|
| #
c1bb746c |
|
13-Dec-2009 |
blanchet <none@none> |
added "no_assms" option to Refute, and include structured proof assumptions by default;
will do the same for Quickcheck unless there are objections
|
| #
95282166 |
|
27-Jul-2009 |
wenzelm <none@none> |
proper context for SAT tactics;
eliminated METAHYPS;
tuned signatures;
|
| #
b1258973 |
|
16-Mar-2009 |
wenzelm <none@none> |
simplified method setup;
|
| #
77d6b267 |
|
13-Mar-2009 |
wenzelm <none@none> |
unified type Proof.method and pervasive METHOD combinators;
|
| #
02d2f437 |
|
02-Apr-2008 |
haftmann <none@none> |
tuned imports
|
| #
f7800759 |
|
29-Nov-2006 |
wenzelm <none@none> |
simplified method setup;
|
| #
3eb67878 |
|
09-Oct-2005 |
webertj <none@none> |
Tactics sat and satx reimplemented, several improvements
|
| #
8a406957 |
|
29-Sep-2005 |
wenzelm <none@none> |
explicit dependencies of SAT vs. Refute;
removed unused methods;
|
| #
e1886398 |
|
24-Sep-2005 |
webertj <none@none> |
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
|
| #
74e3ce8f |
|
24-Sep-2005 |
webertj <none@none> |
cnf_struct renamed to cnf
|
| #
9a31fcb4 |
|
24-Sep-2005 |
obua <none@none> |
preliminary fix of HOL build problem
|
| #
18cfca39 |
|
23-Sep-2005 |
webertj <none@none> |
new sat tactic imports resolution proofs from zChaff
|