| Mon, 04 Apr 2011 14:37:20 +0200 | blanchet | use the proper contexts/simpsets/etc. in the TPTP proof method | file | diff | annotate |
| Mon, 04 Apr 2011 13:27:34 +0200 | blanchet | make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option | file | diff | annotate |
| Thu, 24 Mar 2011 17:49:27 +0100 | blanchet | specify proper defaults for Nitpick and Refute on TPTP + tuning | file | diff | annotate |
| Wed, 23 Mar 2011 20:57:37 +0100 | wenzelm | isolate change of Proofterm.proofs in TPTP.thy from rest of session; | file | diff | annotate |
| Wed, 23 Mar 2011 10:06:27 +0100 | blanchet | move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" | file | diff | annotate | base |