[isabelle-dev] Purpose of guess_infix

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Sep 16 15:24:09 CEST 2018

Hi Makarius,

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
> Isabelle/10da16970d82.
> 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
> description:
> 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.
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180916/78b52714/attachment.sig>

More information about the isabelle-dev mailing list