Thu, 15 May 2014 16:38:29 +0200 | haftmann | modernized setup | changeset | files |
Thu, 15 May 2014 16:38:29 +0200 | haftmann | dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor | changeset | files |
Thu, 15 May 2014 16:38:28 +0200 | haftmann | unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches | changeset | files |
Thu, 15 May 2014 16:38:17 +0200 | haftmann | normalize type variables of evaluation term by conversion | changeset | files |
Thu, 15 May 2014 20:48:14 +0200 | blanchet | more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix) | changeset | files |
Thu, 15 May 2014 20:48:13 +0200 | blanchet | new approach to silence proof methods, to avoid weird theory/context mismatches | changeset | files |