Fri, 22 Dec 1995 11:09:28 +0100 | paulson | Improving space efficiency of inductive/datatype definitions. | changeset | files |
Fri, 22 Dec 1995 10:48:59 +0100 | paulson | Addition of compression, that is, sharing. | changeset | files |
Fri, 22 Dec 1995 10:38:27 +0100 | paulson | Commented the datatype declaration of thm. | changeset | files |