| Mon, 14 Jul 1997 12:42:28 +0200 | paulson | Removed redundant addsimps of Un_insert_left, which is now a default simprule | changeset | files |
| Fri, 11 Jul 1997 13:32:39 +0200 | paulson | Removal of monotonicity reasoning involving "lost" and the theorem | changeset | files |
| Fri, 11 Jul 1997 13:30:01 +0200 | paulson | Now uses the Notes constructor to distinguish the Client (who has chosen M) | changeset | files |