Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-01-10 Thread Makarius
On 10/01/2019 16:28, Florian Haftmann wrote: > 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. > > This

[isabelle-dev] NEWS: generated code as proper theory export

2019-01-10 Thread Florian Haftmann
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. This refers to e02bdf853a4c and opens opportunities to get