Mon, 14 Jun 2010 16:17:20 +0200 | blanchet | improve ATP-specific error messages | changeset | files |
Mon, 14 Jun 2010 15:10:50 +0200 | haftmann | merged | changeset | files |
Mon, 14 Jun 2010 15:10:36 +0200 | haftmann | removed simplifier congruence rule of "prod_case" | changeset | files |
Mon, 14 Jun 2010 10:36:01 +0200 | blanchet | adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf" | changeset | files |