src/HOL/Sledgehammer.thy
2010-06-25 blanchet 2010-06-25 more moving around of ML files in "Sledgehammer.thy"
2010-06-25 blanchet 2010-06-25 move "MESON" up; the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti
2010-06-24 blanchet 2010-06-24 never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
2010-06-23 blanchet 2010-06-23 killed legacy "neg_clausify" and "clausify"
2010-06-22 blanchet 2010-06-22 factor out TPTP format output into file of its own, to facilitate further changes
2010-06-14 blanchet 2010-06-14 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-11 blanchet 2010-06-11 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-04-30 blanchet 2010-04-30 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
2010-04-25 blanchet 2010-04-25 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
2010-04-23 blanchet 2010-04-23 now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
2010-04-23 blanchet 2010-04-23 renamed module "ATP_Wrapper" to "ATP_Systems"
2010-04-23 blanchet 2010-04-23 move the minimizer to the Sledgehammer directory
2010-03-29 blanchet 2010-03-29 added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
2010-03-29 blanchet 2010-03-29 get rid of Polyhash, since it's no longer used
2010-03-24 blanchet 2010-03-24 add new file "sledgehammer_util.ML" to setup
2010-03-19 blanchet 2010-03-19 move all ATP setup code into ATP_Wrapper
2010-03-19 blanchet 2010-03-19 move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later
2010-03-19 blanchet 2010-03-19 more Sledgehammer refactoring
2010-03-17 blanchet 2010-03-17 renamed "ATP_Linkup" theory to "Sledgehammer"