| 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 |