changeset 11097 | c1be9f2dff4c |
parent 11094 | b803ef642e60 |
child 11112 | 2fea4923864f |
--- a/NEWS Sun Feb 11 16:31:54 2001 +0100 +++ b/NEWS Sun Feb 11 16:34:20 2001 +0100 @@ -90,6 +90,8 @@ * Pure: ?thesis / ?this / "..." now work for pure meta-level statements as well; +* Pure: more robust selection of calculational rules; + * Pure: the builtin notion of 'finished' goal now includes the ==-refl rule (as well as the assumption rule);