Fri, 08 Apr 2011 19:04:08 +0200 | boehmes | use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables) | changeset | files |
Fri, 08 Apr 2011 19:04:08 +0200 | boehmes | fixed eta-expansion: use correct order to apply new bound variables | changeset | files |
Fri, 08 Apr 2011 19:04:08 +0200 | boehmes | check if negating the goal is possible (avoids CTERM exception for Pure propositions) | changeset | files |