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...
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)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and