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 |