| Wed, 15 Dec 2010 11:26:28 +0100 | blanchet | added "type_sys" option to Sledgehammer | file | diff | annotate |
| Wed, 08 Dec 2010 22:17:53 +0100 | blanchet | implicitly call the minimizer for SMT solvers that don't return an unsat core | file | diff | annotate |
| Wed, 08 Dec 2010 22:17:52 +0100 | blanchet | clarified terminology | file | diff | annotate |
| Tue, 26 Oct 2010 21:01:28 +0200 | blanchet | standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module | file | diff | annotate |
| Tue, 26 Oct 2010 10:57:04 +0200 | blanchet | no need to encode theorem number twice in skolem names | file | diff | annotate |
| Fri, 22 Oct 2010 18:31:45 +0200 | blanchet | tuning | file | diff | annotate |
| Fri, 22 Oct 2010 14:10:32 +0200 | blanchet | fixed signature of "is_smt_solver_installed"; | file | diff | annotate |
| Fri, 22 Oct 2010 13:57:54 +0200 | blanchet | renamed modules | file | diff | annotate |
| Fri, 22 Oct 2010 13:54:51 +0200 | blanchet | renamed files | file | diff | annotate | base |