| Tue, 28 Sep 2010 11:59:52 +0200 | bulwahn | only modes but not types are used to destruct terms and types; this allows to interpret arguments that are predicates simply as input | changeset | files |
| Tue, 28 Sep 2010 11:59:51 +0200 | bulwahn | weakening check for higher-order relations, but adding check for consistent modes | changeset | files |
| Tue, 28 Sep 2010 11:59:51 +0200 | bulwahn | handling higher-order relations in output terms; improving proof procedure; added test case | changeset | files |