| Thu, 10 Sep 1998 17:26:53 +0200 | paulson | tidied, eliminating hard proof | changeset | files |
| Thu, 10 Sep 1998 17:26:16 +0200 | paulson | well-formed zless_asym; tidied | changeset | files |
| Thu, 10 Sep 1998 17:25:13 +0200 | paulson | patch to stop failing proof | changeset | files |
| Thu, 10 Sep 1998 17:23:51 +0200 | paulson | New theorem wf_not_sym and well-formed wf_asym | changeset | files |
| Thu, 10 Sep 1998 17:23:16 +0200 | paulson | tided the unused rule irrefl_tranclI | changeset | files |
| Thu, 10 Sep 1998 17:20:49 +0200 | paulson | Changed equals0E back to equals0D and gave it the correct destruct form | changeset | files |
| Thu, 10 Sep 1998 17:17:22 +0200 | paulson | Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED | changeset | files |