[isabelle] Precedences question
I defined a function called typeof, which I would like to use with the
syntax "\<tau>" .
So I defined the syntax
"_tau" :: "Value \<Rightarrow> Javatype" ("\<tau> _" 1000)
"\<tau> v" == "typeof v"
But whatever priority I give above, I have to put parentheses around
all occurrences of "\<tau> x" in order to avoid getting ambiguous
syntax, although I can write "typeof x" without the parentheses.
Is this some kind of Isabelle function application precedence magic?
How can I define the syntax to behave in the same way as the original
Thanks a lot in advance
This archive was generated by a fusion of
Pipermail (Mailman edition) and