paulson [Mon, 07 Sep 2009 13:19:09 +0100] rev 32532
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson [Mon, 07 Sep 2009 11:44:12 +0100] rev 32531
merged
paulson [Mon, 07 Sep 2009 10:04:17 +0100] rev 32530
conflict resolution possibly
paulson [Fri, 04 Sep 2009 11:37:24 +0100] rev 32529
New method, metisFT: a fully-typed proof search that should eliminate type errors during reconstruction
paulson [Fri, 28 Aug 2009 13:32:20 +0100] rev 32528
merged
paulson [Thu, 27 Aug 2009 15:49:45 +0100] rev 32527
More streamlining using metis.
nipkow [Mon, 07 Sep 2009 08:32:22 +0200] rev 32526
enabled metis permanently, tuned stats
boehmes [Sat, 05 Sep 2009 22:01:31 +0200] rev 32525
added signature ATP_MINIMAL,
fixed AtpMinimal.minimalize for the trivial case,
Mirabelle: added an option to minimize a theorem set found by sledgehammer,
use timeout of sledgehammer instead of additional timeLimit
boehmes [Sat, 05 Sep 2009 17:35:05 +0200] rev 32524
merged
boehmes [Sat, 05 Sep 2009 17:34:30 +0200] rev 32523
separate output of ATP user time and sledgehammer (ML code) user time