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 |
Fri, 13 Jun 1997 10:04:37 +0200 | mueller | changed compatible definition; | changeset | files |
Thu, 12 Jun 1997 16:48:03 +0200 | mueller | added deadlock | changeset | files |
Thu, 12 Jun 1997 16:47:15 +0200 | mueller | added deadlock freedom, polished definitions and proofs | changeset | files |
Mon, 09 Jun 1997 10:21:38 +0200 | paulson | Strengthened and streamlined the Yahalom proofs | changeset | files |