| Thu, 13 May 2010 00:44:48 +0200 | boehmes | more precise dependencies | changeset | files |
| Wed, 12 May 2010 23:54:06 +0200 | boehmes | updated SMT certificates | changeset | files |
| Wed, 12 May 2010 23:54:04 +0200 | boehmes | layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable | changeset | files |
| Wed, 12 May 2010 23:54:02 +0200 | boehmes | integrated SMT into the HOL image | changeset | files |
| Wed, 12 May 2010 23:54:01 +0200 | boehmes | replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite | changeset | files |
| Wed, 12 May 2010 23:54:00 +0200 | boehmes | use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting) | changeset | files |