| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 12:09:51 +0100 |
blanchet |
delayed construction of command (and of noncommercial check) + tuning
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 11:15:46 +0100 |
blanchet |
undo rewrite rules (e.g. for 'fun_app') in Isar
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 14:48:20 +0100 |
blanchet |
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
thread through step IDs from Z3 to Sledgehammer
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
let exception pass through in debug mode
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
adapted to renamed ML files
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
have Sledgehammer generate Isar proofs from Z3 proofs
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
tuned ML interface
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
integrate SMT2 with Sledgehammer
|
file |
diff |
annotate
|