| Tue, 03 Jun 2014 11:43:07 +0200 |
blanchet |
removed SMT weights -- their impact was very inconclusive anyway
|
file |
diff |
annotate
|
| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 14:48:20 +0100 |
blanchet |
avoid name clash
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 14:48:20 +0100 |
blanchet |
simplify index handling
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 14:48:20 +0100 |
blanchet |
more robust indices
|
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 14:48:20 +0100 |
blanchet |
move lemmas to theory file, towards textual proof reconstruction
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
tuning
|
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 |
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
|
file |
diff |
annotate
|