Wed, 07 May 2008 10:59:47 +0200 | berghofe | eq_assumption now uses aeconv instead of aconv. | changeset | files |
Wed, 07 May 2008 10:59:46 +0200 | berghofe | - Removed function eta_contract_atom, which did not quite work | changeset | files |
Wed, 07 May 2008 10:59:45 +0200 | berghofe | Replaced Pattern.eta_contract_atom by Envir.eta_contract. | changeset | files |
Wed, 07 May 2008 10:59:44 +0200 | berghofe | Removed instantiation for set. | changeset | files |
Wed, 07 May 2008 10:59:43 +0200 | berghofe | Explicitely applied ext in proof of tnd. | changeset | files |
Wed, 07 May 2008 10:59:42 +0200 | berghofe | Deleted subset_antisym in a few proofs, because it is | changeset | files |
Wed, 07 May 2008 10:59:41 +0200 | berghofe | - Tuned imports | changeset | files |