NEWS

--- a/NEWS	Thu Apr 13 15:02:02 2000 +0200
+++ b/NEWS	Thu Apr 13 15:02:57 2000 +0200
@@ -8,6 +8,9 @@
 
 * HOL: the constant for f``x is now "image" rather than "op ``".
 
+* HOL: the cartesian product is now "<*>" instead of "Times".
+       the lexicographic product is now "<*lex*>" instead of "**".
+
 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
 
 * HOL: simplification no longer dives into case-expressions