| Thu, 14 Jul 2011 15:14:38 +0200 |
blanchet |
use monomorphic encoding as fallback, since they tend to produce fewer type errors
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:38 +0200 |
blanchet |
don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
clearer unsound message
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
clarify fine soundness point
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
always unfold "Let"s is Sledgehammer, Metis, and MESON
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
unbreak Nitrox's parsing
|
changeset |
files
|
| Thu, 14 Jul 2011 00:21:56 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 14 Jul 2011 00:20:43 +0200 |
haftmann |
tuned lemma positions and proofs
|
changeset |
files
|
| Thu, 14 Jul 2011 00:16:41 +0200 |
haftmann |
tuned notation
|
changeset |
files
|
| Wed, 13 Jul 2011 23:49:56 +0200 |
haftmann |
uniqueness lemmas for bot and top
|
changeset |
files
|
| Wed, 13 Jul 2011 23:41:13 +0200 |
haftmann |
adjusted to tightened specification of classes bot and top
|
changeset |
files
|
| Wed, 13 Jul 2011 19:43:12 +0200 |
haftmann |
moved lemmas bot_less and less_top to classes bot and top respectively
|
changeset |
files
|