| Tue, 28 Sep 2010 11:59:58 +0200 | bulwahn | using SUBPROOF to ensure that rewriting is not done on the further subgoals of proof | changeset | files |
| Tue, 28 Sep 2010 11:59:57 +0200 | bulwahn | avoiding instable rotate_tac and using the nice Subgoal.FOCUS_PREMS instead | changeset | files |
| Tue, 28 Sep 2010 11:59:53 +0200 | bulwahn | adding test case for interpretation of arguments that are predicates simply as input | changeset | files |
| 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 |