Sat, 21 Dec 2013 09:44:29 +0100 | blanchet | made tactic work with theorems with multiple assumptions | changeset | files |
Sat, 21 Dec 2013 09:44:28 +0100 | blanchet | renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package) | changeset | files |