| Mon, 16 Jun 1997 14:25:33 +0200 | paulson | Type constraint added to ensure that "length" refers to lists. Maybe should | changeset | files |
| Mon, 16 Jun 1997 14:24:11 +0200 | paulson | Replacing the primrec definition of "length" by a translation to the built-in | changeset | files |
| Fri, 13 Jun 1997 10:35:13 +0200 | nipkow | Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas. | changeset | files |