| Tue, 02 Jan 2018 16:17:13 +0100 | blanchet | moved 'realizers' into their own theory, now that they are decupled from the old datatype construction | changeset | files |
| Tue, 02 Jan 2018 16:11:20 +0100 | blanchet | removed 'old_datatype' command | changeset | files |
| Tue, 02 Jan 2018 16:08:59 +0100 | blanchet | don't test 'old_datatype', which is on its way out | changeset | files |
| Tue, 02 Jan 2018 16:01:03 +0100 | blanchet | ported inductive realizer to new datatype package | changeset | files |
| Tue, 02 Jan 2018 15:01:06 +0100 | blanchet | removed needless theorems | changeset | files |
| Tue, 02 Jan 2018 14:42:00 +0100 | blanchet | store high-level 'size' equations | changeset | files |