| Tue, 20 Mar 2012 10:21:05 +0100 |
blanchet |
tune Metis example
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 19:34:52 +0100 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuned Metis examples
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
Metis examples use the new Skolemizer to test it
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| 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, 01 Sep 2010 00:07:31 +0200 |
blanchet |
rename sledgehammer config attributes
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 18:47:07 +0200 |
blanchet |
no setup is necessary anymore
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 01:11:06 +0200 |
blanchet |
more neg_clausify proofs that get replaced by direct proofs
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 21:28:27 +0100 |
wenzelm |
modernized some syntax translations;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 19:52:04 +0200 |
wenzelm |
modernized session Metis_Examples;
|
file |
diff |
annotate
| base
|