Fri, 16 Dec 2016 22:54:14 +0100 | blanchet | refactored induction principle generation code, for reuse for nonuniform datatypes | changeset | files |
Fri, 16 Dec 2016 19:50:46 +0100 | wenzelm | merged | changeset | files |
Fri, 16 Dec 2016 19:07:16 +0100 | wenzelm | consolidate nested thms with persistent result, for improved performance; | changeset | files |