| Thu, 28 Dec 1995 12:37:00 +0100 |
paulson |
Purely cosmetic changes
|
changeset |
files
|
| Thu, 28 Dec 1995 12:36:05 +0100 |
paulson |
Updated comments for compression functions
|
changeset |
files
|
| Thu, 28 Dec 1995 11:59:40 +0100 |
paulson |
Removed unfold:thm from signature INTR_ELIM and from the
|
changeset |
files
|
| Thu, 28 Dec 1995 11:59:15 +0100 |
paulson |
Now mutual_induct is simply "True" unless it is going to be
|
changeset |
files
|
| Thu, 28 Dec 1995 11:54:15 +0100 |
paulson |
fixed indentation
|
changeset |
files
|
| Sat, 23 Dec 1995 12:50:53 +0100 |
nipkow |
New version of type sections and many small changes.
|
changeset |
files
|
| Fri, 22 Dec 1995 13:38:57 +0100 |
paulson |
Note that unfold is not exported, that mutual_induct can
|
changeset |
files
|
| 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
|