Re: [isabelle] Follow-up [Re: Isabelle operator precedence]



You have prompted me to add a table of infix operators to the existing "What's
in Main" manual (development version). In the process I have also fixed a few
odd associativities, mostly making a few predicates non-associative. The table
differs from yours in a number of respects. I am still debating if the framework
operators like ==> should be in there too, although they come not from HOL but Pure.

Thanks for your prompt.
Tobias

Am 12/11/2012 23:05, schrieb Holger Blasum:
> Dear all, 
> 
> 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.
> 
> Best,
> 





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