src/HOL/ex/SAT_Examples.thy
Fri, 17 May 2013 20:41:45 +0200 wenzelm proper option quick_and_dirty;
Tue, 05 Mar 2013 13:03:24 +0100 webertj Avoid ML warning about unreferenced identifier.
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup;
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Sat, 08 Jan 2011 16:01:51 +0100 wenzelm modernized structure Prop_Logic;
Fri, 27 Aug 2010 14:07:09 +0200 wenzelm expanded some aliases from structure Unsynchronized;
Tue, 17 Aug 2010 17:57:19 +0100 webertj Tuned.
Sat, 07 Nov 2009 18:55:30 +0000 webertj Due to popular demand: added a function that benchmarks proof reconstruction
Sat, 17 Oct 2009 16:33:14 +0200 wenzelm Unsynchronized.set etc.;
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;
Fri, 06 Jul 2007 17:21:18 +0200 webertj cosmetic (line length fixed)
Wed, 10 Jan 2007 19:18:29 +0100 webertj minor comment change
Wed, 29 Nov 2006 15:44:51 +0100 wenzelm simplified method setup;
Sun, 19 Nov 2006 13:02:55 +0100 webertj profiling disabled
Wed, 30 Aug 2006 16:27:53 +0200 webertj faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
Wed, 02 Aug 2006 00:57:41 +0200 webertj proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
Tue, 01 Aug 2006 15:28:55 +0200 webertj comment (timing information for last example) added
Mon, 17 Jul 2006 00:37:06 +0200 webertj support for MiniSat proof traces added
Fri, 07 Jul 2006 18:13:58 +0200 webertj "solver" reference added to make the SAT solver configurable
Mon, 03 Jul 2006 17:17:41 +0200 webertj CNF tactic invocations moved into comments
Tue, 02 May 2006 19:23:48 +0200 webertj beta_eta_conversion added to pre_cnf_tac
Fri, 10 Mar 2006 16:31:50 +0100 webertj clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
Sun, 09 Oct 2005 17:06:03 +0200 webertj Tactics sat and satx reimplemented, several improvements
Sat, 24 Sep 2005 07:21:46 +0200 webertj code reformatted and restructured, many minor modifications
Fri, 23 Sep 2005 22:58:50 +0200 webertj new sat tactic imports resolution proofs from zChaff
less more (0) tip