[isabelle-dev] Purpose of guess_infix
makarius at sketis.net
Sat Sep 15 21:32:35 CEST 2018
What is the purpose of guess_infix? It appears to be unused in current
It orgininates from the following changeset:
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.
More information about the isabelle-dev