| 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 |
| Fri, 13 Jun 1997 10:04:37 +0200 | mueller | changed compatible definition; | changeset | files |