NEWS
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 "**";