Mon, 26 Apr 2010 23:45:32 +0200 fixes 2a5c6e7b55cb;
blanchet [Mon, 26 Apr 2010 23:45:32 +0200] rev 36406
fixes 2a5c6e7b55cb; do not throw out the baby with the bath water
Mon, 26 Apr 2010 21:50:36 +0200 compile
blanchet [Mon, 26 Apr 2010 21:50:36 +0200] rev 36405
compile
Mon, 26 Apr 2010 21:41:54 +0200 make compile (and not just load dynamically)
blanchet [Mon, 26 Apr 2010 21:41:54 +0200] rev 36404
make compile (and not just load dynamically)
Mon, 26 Apr 2010 21:25:32 +0200 merge
blanchet [Mon, 26 Apr 2010 21:25:32 +0200] rev 36403
merge
Mon, 26 Apr 2010 21:20:43 +0200 introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet [Mon, 26 Apr 2010 21:20:43 +0200] rev 36402
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method; the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure
Mon, 26 Apr 2010 21:18:20 +0200 adapt code to reflect new signature of "neg_clausify"
blanchet [Mon, 26 Apr 2010 21:18:20 +0200] rev 36401
adapt code to reflect new signature of "neg_clausify"
Mon, 26 Apr 2010 21:17:41 +0200 rename options and keep track of conjecture shape (to facilitate proof reconstruction)
blanchet [Mon, 26 Apr 2010 21:17:41 +0200] rev 36400
rename options and keep track of conjecture shape (to facilitate proof reconstruction)
Mon, 26 Apr 2010 21:17:04 +0200 rename options
blanchet [Mon, 26 Apr 2010 21:17:04 +0200] rev 36399
rename options
Mon, 26 Apr 2010 21:16:35 +0200 make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet [Mon, 26 Apr 2010 21:16:35 +0200] rev 36398
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
Mon, 26 Apr 2010 21:14:28 +0200 remove needless code that was copy-pasted from Quickcheck (where it made sense)
blanchet [Mon, 26 Apr 2010 21:14:28 +0200] rev 36397
remove needless code that was copy-pasted from Quickcheck (where it made sense)
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip