Re: [isabelle] Follow-up [Re: Isabelle operator precedence]
On Mon, 12 Nov 2012, Holger Blasum wrote:
attached is an attempt to follow-up on last week's discussion (thanks!).
I think it is good enough for myself at the moment, however in case sth
like this would make it into user documentation note that there are
still some gaps e.g. concerning precedence values e.g. of "set"/"list"
type constructors or the application of user-defined functions.
Type => and \<lambda> is also "metalogic" in your categorisation, also the
"::" notation for type and sort constraints. Isabelle/HOL re-uses the
Pure type system for its purposes. Pure notation has rather low syntax
priorities, which explains why it is all at the bottom of your list.
This archive was generated by a fusion of
Pipermail (Mailman edition) and