--- a/NEWS Sun Jan 13 19:42:06 2019 +0100
+++ b/NEWS Sun Jan 13 20:25:41 2019 +0100
@@ -75,9 +75,10 @@
*** HOL ***
* Code generation: command 'export_code' without file keyword exports
-code as regular theory export, which can be materialized using tool
-'isabelle export'; to get generated code dumped into output, use
-'file ""'. Minor INCOMPATIBILITY.
+code as regular theory export, which can be materialized using the
+command-line tool "isabelle export", or browsed in Isabelle/jEdit via
+the "isabelle-export:" file-system. To get generated code dumped into
+output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
* Simplified syntax setup for big operators under image. In rare
situations, type conversions are not inserted implicitly any longer