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 |