Re: [isabelle] Isabelle operator precedence



The precedence information is attached to the definition/introduction of each
operator. In HOL.thy you find that "=" has precedence 50 and \<inter> has
precedence 70 (missing from your document). Then there is also the associativity.

I wouldn't exactly call this reverse engineering, but collecting this
information would be useful. I guess "What's in Main" is the right document this
could go into. When I find the time...

Tobias

Am 05/11/2012 15:23, schrieb Holger Blasum:
> Dear all,
> 
> while it is mostly "intuitive" I would like to have a clearer view of 
> operator precedence in Isabelle. Attached is what I quickly reverse-
> engineered on a train ride on the long weekend. Is it correct? Is there 
> already any explicit information on this (beyond using 
> Isabelle -> Settings -> Display -> Show Brackets in PG)?
> 
> Thanks,
> 





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