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.
Cheers,
Florian
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-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
