*** empty log message ***
authornipkow
Thu, 13 Apr 2000 15:02:57 +0200
changeset 8705 a3da5538d924
parent 8704 f76f41f24c44
child 8706 d81088481ec6
*** empty log message ***
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