src/HOL/ATP.thy
2011-11-16 blanchet 2011-11-16 compile
2011-08-09 blanchet 2011-08-09 load lambda-lifting structure earlier, so it can be used in Metis
2011-07-05 nik 2011-07-05 improved translation of lambdas in THF
2011-05-31 blanchet 2011-05-31 use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2010-10-26 blanchet 2010-10-26 reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
2010-10-25 haftmann 2010-10-25 moved sledgehammer to Plain; tuned dependencies
2010-10-05 blanchet 2010-10-05 tuned comments
2010-10-05 blanchet 2010-10-05 factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure