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