src/HOL/Tools/Sledgehammer/metis_clauses.ML
Tue, 29 Jun 2010 09:05:37 +0200 blanchet move functions not needed by Metis out of "Metis_Clauses"
Mon, 28 Jun 2010 18:15:40 +0200 blanchet remove obsolete component of CNF clause tuple (and reorder it)
Mon, 28 Jun 2010 18:02:36 +0200 blanchet get rid of Skolem cache by performing CNF-conversion after fact selection
Mon, 28 Jun 2010 17:31:38 +0200 blanchet always perform relevance filtering on original formulas
Fri, 25 Jun 2010 17:08:39 +0200 blanchet renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
less more (0) tip