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

As a current learner of Isabelle: Please include the Pure operators
(though marking them as not from HOL makes sense). I think this is
important because they appear mixed with HOL operators frequently, so
having it all in one place is useful and avoids confusion. Just
because an operator is actually from the underlying Pure does not
change the fact that it is part of the normal HOL style and workflow,
so it still belongs in such a list. Also it's useful for comparison
with the HOL operators.


On Mon, Dec 17, 2012 at 11:34 AM, Tobias Nipkow <nipkow at> wrote:
> 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.