Tue, 10 Dec 2019 01:06:39 +0100 | traytel | an extensive example for lift_bnf across quotients | changeset | files |
Tue, 10 Dec 2019 01:06:39 +0100 | traytel | extension of lift_bnf to support quotient types | changeset | files |
Tue, 10 Dec 2019 01:06:39 +0100 | traytel | unfold intermediate (internal) pred definitions | changeset | files |
Mon, 09 Dec 2019 16:37:26 +0000 | paulson | corrected some confusing terminology / notation | changeset | files |
Mon, 09 Dec 2019 16:13:36 +0000 | paulson | Ramsey with multiple colours and arbitrary exponents | changeset | files |
Mon, 09 Dec 2019 15:36:51 +0000 | paulson | a few new and tidier proofs (mostly about finite sets) | changeset | files |
Mon, 09 Dec 2019 11:17:34 +0100 | wenzelm | clarified signature: store full theory name; | changeset | files |