| Thu, 14 Jul 2011 22:53:43 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 14 Jul 2011 22:08:11 +0200 |
krauss |
added missing dependencies;
|
changeset |
files
|
| Thu, 14 Jul 2011 19:43:45 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 14 Jul 2011 17:15:24 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 14 Jul 2011 17:14:54 +0200 |
haftmann |
tuned notation and proofs
|
changeset |
files
|
| Thu, 14 Jul 2011 17:29:30 +0200 |
blanchet |
move error logic closer to user
|
changeset |
files
|
| Thu, 14 Jul 2011 17:29:30 +0200 |
blanchet |
allow lambda-lifting without triggers
|
changeset |
files
|
| Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
|
changeset |
files
|
| Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
added option to control which lambda translation to use (for experiments)
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:38 +0200 |
blanchet |
fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem
|
changeset |
files
|
| 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
|
| Wed, 13 Jul 2011 19:40:18 +0200 |
haftmann |
tightened specification of classes bot and top: uniqueness of top and bot elements
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
honor the TPTP environment variable as the root of include relative paths -- that's a weird convention but without it Nitrox will fail at CASC
|
changeset |
files
|