| Wed, 29 Sep 2010 11:36:16 +0200 | bulwahn | merged | changeset | files |
| Wed, 29 Sep 2010 10:33:15 +0200 | bulwahn | adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned | changeset | files |
| Wed, 29 Sep 2010 10:33:15 +0200 | bulwahn | added test case for predicate arguments in higher-order argument position | changeset | files |
| Wed, 29 Sep 2010 10:33:15 +0200 | bulwahn | improving the compilation to handle predicate arguments in higher-order argument positions | changeset | files |
| Wed, 29 Sep 2010 10:33:15 +0200 | bulwahn | added a test case to Predicate_Compile_Tests | changeset | files |
| Wed, 29 Sep 2010 10:33:14 +0200 | bulwahn | putting the last step of the proof in a TRY block to handle the case that the simplifier already solved the goal | changeset | files |
| Wed, 29 Sep 2010 11:02:24 +0200 | krauss | backed out my old attempt at single_hyp_subst_tac (67cd6ed76446) | changeset | files |