src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
2010-12-20 ago optionally supply constant weights to E -- turned off by default until properly parameterized
2010-12-17 ago more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
2010-12-17 ago put the SMT weights back where they belong, so that they're also used by Mirabelle
2010-12-17 ago run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
2010-12-17 ago make timeout part of the SMT filter's tail
2010-12-17 ago split "smt_filter" into head and tail
2010-12-17 ago trap one more Z3 error
2010-12-17 ago more precise/correct SMT error handling
2010-12-16 ago discriminate SMT errors a bit better
2010-12-16 ago no need to do a super-duper atomization if Metis fails afterwards anyway
2010-12-16 ago robustly handle SMT exceptions in Sledgehammer
2010-12-16 ago make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
2010-12-15 ago facilitate debugging
2010-12-15 ago clean up fudge factors a little bit
2010-12-15 ago added weights to SMT problems
2010-12-15 ago honor "overlord" option for SMT solvers as well and don't pass "ext" to them
2010-12-15 ago crank up Metis's timeout for SMT solvers, since users love Metis
2010-12-15 ago generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
2010-12-15 ago added Sledgehammer support for higher-order propositional reasoning
2010-12-15 ago implemented partially-typed "tags" type encoding
2010-12-15 ago implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
2010-12-15 ago added "type_sys" option to Sledgehammer
2010-12-15 ago re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
2010-12-10 ago made smlnj happy
2010-12-08 ago lower fudge factor
2010-12-08 ago implicitly call the minimizer for SMT solvers that don't return an unsat core
2010-12-08 ago renamings
2010-12-08 ago moved function to later module
2010-12-08 ago clarified terminology
2010-12-08 ago split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems