*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] unicode tokens in isabelle2011+pg4.0*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 2 Feb 2011 08:32:30 -0800*Cc*: Joachim Breitner <mail at joachim-breitner.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1102021710090.17057@atbroy100.informatik.tu-muenchen.de>*References*: <FB350234-C48C-4133-AC5C-81C38796D227@cam.ac.uk> <4D4874DC.1070507@in.tum.de> <1296624434.2475.37.camel@kirk> <AANLkTi=AFNNO01fLKAm26V2nK_YwHcVQ7AjXZJ1L_p0N@mail.gmail.com> <alpine.LNX.1.10.1102021710090.17057@atbroy100.informatik.tu-muenchen.de>*Sender*: huffman.brian.c at gmail.com

On Wed, Feb 2, 2011 at 8:15 AM, Makarius <makarius at sketis.net> wrote: > On Wed, 2 Feb 2011, Brian Huffman wrote: > >> On Tue, Feb 1, 2011 at 9:27 PM, Joachim Breitner >> <mail at joachim-breitner.de> wrote: >>> >>> is there a reason why Isabelle would not accept ∀ synonymously to >>> \<forall> in theory files? This would also be nice for all those >>> unicode-loving folk who occasionally at .thy files directly (e.g. doing >>> some mass-substitution with vim, or looking at diffs). >> >> You can certainly configure Isabelle to allow unicode as an alternative >> input syntax. For example, you can define the following notation for the >> forall-quantifier, where "∀" is a genuine unicode symbol instead of the >> "\<forall>" markup: >> >> notation (input) All (binder "∀" 10) >> >> Now the genuine unicode forall symbol works as expected on input: >> >> term "∀x. P x" >> >> I suppose you could create a theory file that defines similar unicode >> notation for all syntax defined in Isabelle/HOL. This might make a nice >> addition to HOL/Library. > > This is a bad idea. From what has been explained before, the Isabelle > treatment of symbols vs. unicode handling assumes that this is not done. Big > confusion is to be expected if this is violated. (E.g. try to load such a > file with Isabelle/jEdit and then save it again.) > > See also http://isabelle.in.tum.de/dist/Isabelle2011/doc/implementation.pdf > section "1.2.1 Strings of Symbols" for some explanations and specifications > around this important Isabelle concept. In section 1.2.1 of the Implementation manual, it clearly states that unicode codepoints like "∀" are treated distinctly from symbols like "\<forall>". ProofGeneral 4.0 and 4.1 apparently respect this distinction, while Isabelle/jEdit does not. - Brian

**References**:**[isabelle] unicode tokens in isabelle2011+pg4.0***From:*John Wickerson

**Re: [isabelle] unicode tokens in isabelle2011+pg4.0***From:*Alexander Krauss

**Re: [isabelle] unicode tokens in isabelle2011+pg4.0***From:*Joachim Breitner

**Re: [isabelle] unicode tokens in isabelle2011+pg4.0***From:*Brian Huffman

**Re: [isabelle] unicode tokens in isabelle2011+pg4.0***From:*Makarius

- Previous by Date: Re: [isabelle] unicode tokens in isabelle2011+pg4.0
- Next by Date: Re: [isabelle] unicode tokens in isabelle2011+pg4.0
- Previous by Thread: Re: [isabelle] unicode tokens in isabelle2011+pg4.0
- Next by Thread: Re: [isabelle] unicode tokens in isabelle2011+pg4.0
- Cl-isabelle-users February 2011 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