src/HOL/Tools/Sledgehammer/metis_translate.ML
2010-09-17 blanchet 2010-09-17 simplify Skolem handling; things are much easier now that Sledgehammer doesn't skolemize, only Metis
2010-09-16 blanchet 2010-09-16 complete refactoring of Metis along the lines of Sledgehammer
2010-09-16 blanchet 2010-09-16 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"