| Thu, 24 Jun 2010 21:04:35 +0200 | haftmann | more direct definition simplifies proofs | changeset | files |
| Thu, 24 Jun 2010 21:03:32 +0200 | haftmann | merged | changeset | files |
| Thu, 24 Jun 2010 18:45:31 +0200 | haftmann | more precise tactic: do not escape to a different goal branch (REPEAT is still problematic, though) | changeset | files |
| Thu, 24 Jun 2010 18:22:15 +0200 | blanchet | a76ace919f1c wasn't quite right; second try | changeset | files |
| Thu, 24 Jun 2010 18:04:31 +0200 | blanchet | merge | changeset | files |
| Thu, 24 Jun 2010 17:57:36 +0200 | blanchet | never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts | changeset | files |
| Thu, 24 Jun 2010 17:27:18 +0200 | blanchet | better eta-expansion in Sledgehammer's clausification; | changeset | files |
| Thu, 24 Jun 2010 17:25:47 +0200 | blanchet | cosmetics | changeset | files |