| Thu, 15 Feb 2007 17:35:19 +0100 | krauss | changed termination goal to use object quantifier | changeset | files |
| Thu, 15 Feb 2007 12:14:34 +0100 | krauss | added congruence rule for function composition | changeset | files |
| Thu, 15 Feb 2007 12:02:11 +0100 | krauss | beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on. | changeset | files |