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