| Thu, 23 Jan 1997 10:34:18 +0100 | paulson | Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result() | changeset | files |
| Wed, 22 Jan 1997 18:17:36 +0100 | nipkow | Added warning msg when the simplifier cannot use a premise as a rewrite rule | changeset | files |
| Tue, 21 Jan 1997 11:29:28 +0100 | nipkow | Modified MiniML. Added W0. | changeset | files |