Thu, 24 Jun 2010 21:01:13 +0200 | blanchet | yields ill-typed ATP/metis proofs -- raus! | changeset | files |
Thu, 24 Jun 2010 21:00:37 +0200 | blanchet | make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars" | changeset | files |
Fri, 25 Jun 2010 07:19:21 +0200 | haftmann | merged | changeset | files |
Thu, 24 Jun 2010 21:04:35 +0200 | haftmann | more direct definition simplifies proofs | changeset | files |