--- a/NEWS Sat Jun 14 15:58:36 2008 +0200
+++ b/NEWS Sat Jun 14 17:26:07 2008 +0200
@@ -15,6 +15,9 @@
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY.
+* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML
+interface instead.
+
*** HOL ***