Re: [isabelle] Follow-up [Re: Isabelle operator precedence]
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Follow-up [Re: Isabelle operator precedence]
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Mon, 17 Dec 2012 18:34:50 +0100
- In-reply-to: <20121112220515.GA6316@laptop-hbl.localdomain>
- References: <20121105142302.GA10786@laptop-hbl.localdomain> <20121112220515.GA6316@laptop-hbl.localdomain>
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:17.0) Gecko/17.0 Thunderbird/17.0
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and