*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] unicode tokens in isabelle2011+pg4.0*From*: Makarius <makarius at sketis.net>*Date*: Wed, 2 Feb 2011 17:15:06 +0100 (CET)*Cc*: Joachim Breitner <mail at joachim-breitner.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTi=AFNNO01fLKAm26V2nK_YwHcVQ7AjXZJ1L_p0N@mail.gmail.com>*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>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

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 alternativeinput syntax. For example, you can define the following notation for theforall-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 unicodenotation for all syntax defined in Isabelle/HOL. This might make a niceaddition to HOL/Library.

Makarius

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

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

**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

- Previous by Date: [isabelle] String.explode in generated code
- 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