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