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

Reply via email to