| Fri, 22 Dec 1995 13:33:40 +0100 | paulson | Added line breaks and other cosmetic changes | changeset | files |
| Fri, 22 Dec 1995 12:25:20 +0100 | nipkow | defined take/drop by induction over list rather than nat. | changeset | files |
| 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 |