src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
Thu, 31 Jan 2013 17:54:05 +0100 blanchet distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
Sat, 19 Jan 2013 17:42:12 +0100 blanchet tuning
Thu, 20 Dec 2012 15:51:27 +0100 blanchet better weight functions for MePo/MaSh etc.
Wed, 05 Dec 2012 13:25:06 +0100 blanchet take proximity into account for MaSh + fix a debilitating bug in feature generation
Wed, 05 Dec 2012 13:25:06 +0100 blanchet tuning
Mon, 12 Nov 2012 14:46:42 +0100 blanchet fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
Fri, 20 Jul 2012 22:43:51 +0200 blanchet tune Mesh filter
Fri, 20 Jul 2012 22:19:46 +0200 blanchet honor suggested MaSh weights
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML structures
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML files
less more (0) tip