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

[Makarius]

On 01/02/2019 16:40, Lars Hupel wrote:
>> The standard approach for the latter is to have the other tool directly
>> import its source format into the theory context within Isabelle/ML,
>> without the intermediate theory source. Doing this carefully, would even
>> produce nice PIDE markup for the original sources. PIDE is an IDE for
>> arbitrary user-defined languages.
>>
>> It might be worth doing this for tools like Lem eventually, but I have
>> not looked at it closely so far.
> 
> Lem is implemented in OCaml, so this seems like a stretch. I'd say
> importing HOL4 into Isabelle is a more plausible solution.

Yes, the motivation behind using Lem is diminished by the promising work
of Fabian Immler.

In general, though, alien tool output can be imported into the formal
context. One merely needs to devise some tricks. A tool implemented in
Haskell or OCaml should be particularly easy.


	Makarius