[isabelle] Precedences question



Hello all,

I defined a function called typeof, which I would like to use with the syntax "\<tau>" .
So I defined the syntax

syntax
 "_tau" :: "Value \<Rightarrow> Javatype" ("\<tau> _" 1000)

translations
 "\<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 function?

Thanks a lot in advance

Nicole








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.