NEWS
changeset 69649 e61b0b819d28
parent 69643 83f15deb2d36
child 69672 f97fbb2330aa
     1.1 --- a/NEWS	Sun Jan 13 19:42:06 2019 +0100
     1.2 +++ b/NEWS	Sun Jan 13 20:25:41 2019 +0100
     1.3 @@ -75,9 +75,10 @@
     1.4  *** HOL ***
     1.5  
     1.6  * Code generation: command 'export_code' without file keyword exports
     1.7 -code as regular theory export, which can be materialized using tool
     1.8 -'isabelle export'; to get generated code dumped into output, use
     1.9 -'file ""'.  Minor INCOMPATIBILITY.
    1.10 +code as regular theory export, which can be materialized using the
    1.11 +command-line tool "isabelle export", or browsed in Isabelle/jEdit via
    1.12 +the "isabelle-export:" file-system. To get generated code dumped into
    1.13 +output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
    1.14  
    1.15  * Simplified syntax setup for big operators under image. In rare
    1.16  situations, type conversions are not inserted implicitly any longer