src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
2014-03-13 ago simplified preplaying information
2014-03-13 ago integrate SMT2 with Sledgehammer
2014-02-13 ago avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
2014-02-13 ago removed hint that is seldom useful in practice
2014-02-04 ago split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
2014-02-04 ago removed legacy 'metisFT' method
2014-02-04 ago tuning
2014-02-03 ago renamed ML file