| Tue, 21 Dec 2010 10:18:56 +0100 |
blanchet |
added "sledgehammer_tac" as possible reconstructor in Mirabelle
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 16:20:02 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
implemented partially-typed "tags" type encoding
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:52 +0100 |
blanchet |
renamings
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:52 +0100 |
blanchet |
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 11:41:24 +0100 |
blanchet |
handle "max_relevant" uniformly
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 18:29:14 +0100 |
blanchet |
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
improving sledgehammer_tactic and adding relevance filtering to the tactic
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:41:55 +0100 |
bulwahn |
ported sledgehammer_tactic to current development version
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:41:53 +0100 |
bulwahn |
adding files to use sledgehammer as a tactic for non-interactive use
|
file |
diff |
annotate
|