| Sat, 09 Apr 2011 15:00:23 +0200 | wenzelm | made SML/NJ happy; | changeset | files |
| Sat, 09 Apr 2011 13:10:20 +0200 | wenzelm | merged | changeset | files |
| Fri, 08 Apr 2011 19:04:08 +0200 | boehmes | added SMT certificates | changeset | files |
| 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 |
| Fri, 08 Apr 2011 19:04:08 +0200 | boehmes | unfold and eta-contract let expressions before lambda-lifting to avoid bad terms | changeset | files |