src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
Wed, 15 Dec 2010 11:26:28 +0100 blanchet weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
Wed, 15 Dec 2010 11:26:28 +0100 blanchet implemented partially-typed "tags" type encoding
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