| 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 |
| Fri, 22 Dec 1995 10:34:54 +0100 | paulson | Removed obsolete alist_of and st_of_alist. | changeset | files |
| Fri, 22 Dec 1995 10:30:06 +0100 | paulson | "prep_const" now calls compress_type to ensure sharing among | changeset | files |
| Fri, 22 Dec 1995 10:26:57 +0100 | paulson | "prepare_proof" has been simplified because | changeset | files |
| Fri, 22 Dec 1995 10:19:55 +0100 | paulson | Now "standard" compresses theorems (for sharing). | changeset | files |