On 16/09/18 15:24, Florian Haftmann wrote:
>
> I guess this had something to do with Haskabelle, taking into account
> its fundamental design flaw to write terms on its own rather than having
> Isabelle's existing printing doing the job.
>
> Since there is no reference left, it can be safely discarded.
>>
>> The motivation behind the question: slightly more high-level access to
>> notation, e.g. for export to other languages; possibly without "fishing"
>> in the generated grammar.
OK, I will replace it by something that I can use for the purpose of
exporting theory content.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
