[isabelle-dev] Purpose of guess_infix
florian.haftmann at informatik.tu-muenchen.de
Sun Sep 16 15:24:09 CEST 2018
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.
Am 15.09.2018 um 21:32 schrieb Makarius:
> What is the purpose of guess_infix? It appears to be unused in current
> It orgininates from the following changeset:
> changeset: 26678:a3ae088dc20f
> user: haftmann
> date: Wed Apr 16 10:50:37 2008 +0200
> files: src/Pure/Syntax/parser.ML src/Pure/Syntax/syntax.ML
> educated guess for infix syntax
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev