changeset 10065 | ddb3a014f721 |
parent 10003 | bd2ef19a0275 |
child 10080 | 8fb8c17d1cb5 |
--- a/NEWS Sat Sep 23 16:02:01 2000 +0200 +++ b/NEWS Sat Sep 23 16:08:23 2000 +0200 @@ -45,6 +45,8 @@ * HOL: the constant for "f``x" is now "image" rather than "op ``"; +* HOL: the constant for "f-``x" is now "vimage" rather than "op -``"; + * HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian product is now "<*>" instead of "Times"; the lexicographic product is now "<*lex*>" instead of "**";