Tue, 22 May 2012 16:59:27 +0200 | blanchet | added one slice with configurable simplification turned off | changeset | files |
Tue, 22 May 2012 16:59:27 +0200 | blanchet | make higher-order goals more first-order via extensionality | changeset | files |
Tue, 22 May 2012 16:59:27 +0200 | blanchet | added "ext_cong_neq" lemma (not used yet); tuning | changeset | files |