*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Isabelle operator precedence*From*: Makarius <makarius at sketis.net>*Date*: Thu, 15 Nov 2012 16:54:26 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <509D1C70.7050308@in.tum.de>*References*: <20121105142302.GA10786@laptop-hbl.localdomain> <CAAMXsiaSBptcj3swFrbBFAOZdZ=iSZhJRQEwbC5wBLeRy_v7QQ@mail.gmail.com> <20121105195910.GA14984@laptop-hbl.localdomain> <509871D7.3030509@jaist.ac.jp> <509D1C70.7050308@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 9 Nov 2012, Tobias Nipkow wrote:

Am 06/11/2012 03:11, schrieb Christian Sternagel:Again, when both arguments have the same precedence it means that the operator is non-associative, try, e.g., to enter term "x ≠ x ≠ y" (Note that this only works with the xsymbol for not-equal, since the ASCII symbol ~= is declared as "infixl", i.e., left-associative infix operator.)I noticed this too, when compiling the table of infix operators. This isweird and should be cleared up. In fact, = and ~= and ≠ should all benon-associative because there is no canonical orientation.

Makarius

**References**:**[isabelle] Isabelle operator precedence***From:*Holger Blasum

**Re: [isabelle] Isabelle operator precedence***From:*Brian Huffman

**Re: [isabelle] Isabelle operator precedence***From:*Holger Blasum

**Re: [isabelle] Isabelle operator precedence***From:*Christian Sternagel

**Re: [isabelle] Isabelle operator precedence***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Exporting Proof Terms to Text File
- Next by Date: Re: [isabelle] Highlight sorry in jEdit
- Previous by Thread: Re: [isabelle] Isabelle operator precedence
- Next by Thread: Re: [isabelle] Isabelle operator precedence
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list