Mon, 30 Aug 2010 11:39:23 +0200 blanchet deal with duplicates
Mon, 30 Aug 2010 11:11:10 +0200 blanchet improve new "sledgehammer_filter" action
Mon, 30 Aug 2010 11:10:44 +0200 blanchet remove useless var
Mon, 30 Aug 2010 10:26:17 +0200 blanchet added evaluation method for relevance filter
Mon, 30 Aug 2010 09:41:59 +0200 blanchet remove needless parameter
Mon, 30 Aug 2010 08:53:27 +0200 blanchet bring Sledgehammer's combinators in line with Metis's;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip