| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added example to exercise higher-order reasoning with Sledgehammer and Metis
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 19:21:46 +0200 |
haftmann |
modernized primrec
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 00:07:31 +0200 |
blanchet |
rename sledgehammer config attributes
|
file |
diff |
annotate
|
| Tue, 11 May 2010 19:21:05 +0200 |
hoelzl |
Removed usage of normalizating locales.
|
file |
diff |
annotate
|
| Fri, 07 May 2010 09:59:24 +0200 |
haftmann |
prefix normalizing replaces class_semiring
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 14:00:09 +0200 |
blanchet |
minor improvements
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:49:52 +0200 |
blanchet |
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 18:07:51 +0200 |
blanchet |
redid the proofs with the latest Sledgehammer;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 19:52:04 +0200 |
wenzelm |
modernized session Metis_Examples;
|
file |
diff |
annotate
| base
|