# HG changeset patch
# User nipkow
# Date 955630977 -7200
# Node ID a3da5538d9245637270d706a7912ba12114974f1
# Parent  f76f41f24c44986c0ac6cfabe846e4a84e0a65fc
*** empty log message ***

diff -r f76f41f24c44 -r a3da5538d924 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