src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
Wed, 08 Dec 2010 22:18:37 +0100 blanchet lower fudge factor
Wed, 08 Dec 2010 22:17:53 +0100 blanchet implicitly call the minimizer for SMT solvers that don't return an unsat core
Wed, 08 Dec 2010 22:17:52 +0100 blanchet renamings
Wed, 08 Dec 2010 22:17:52 +0100 blanchet moved function to later module
Wed, 08 Dec 2010 22:17:52 +0100 blanchet clarified terminology
Wed, 08 Dec 2010 22:17:52 +0100 blanchet split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
less more (0) tip