src/HOL/Tools/Sledgehammer/metis_clauses.ML
2010-06-29 blanchet 2010-06-29 rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
2010-06-29 blanchet 2010-06-29 move "nice names" from Metis to TPTP format
2010-06-29 blanchet 2010-06-29 move functions not needed by Metis out of "Metis_Clauses"
2010-06-28 blanchet 2010-06-28 remove obsolete component of CNF clause tuple (and reorder it)
2010-06-28 blanchet 2010-06-28 get rid of Skolem cache by performing CNF-conversion after fact selection
2010-06-28 blanchet 2010-06-28 always perform relevance filtering on original formulas
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer