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