Tue, 26 Oct 2010 12:17:19 +0200 | blanchet | reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers | file | diff | annotate |
Mon, 25 Oct 2010 13:34:57 +0200 | haftmann | moved sledgehammer to Plain; tuned dependencies | file | diff | annotate |
Tue, 05 Oct 2010 12:50:45 +0200 | blanchet | tuned comments | file | diff | annotate |
Tue, 05 Oct 2010 11:10:37 +0200 | blanchet | factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure | file | diff | annotate |