[isabelle-dev] Purpose of guess_infix

[Makarius]

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