*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] unicode tokens in isabelle2011+pg4.0*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 2 Feb 2011 06:21:25 -0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1296624434.2475.37.camel@kirk>*References*: <FB350234-C48C-4133-AC5C-81C38796D227@cam.ac.uk> <4D4874DC.1070507@in.tum.de> <1296624434.2475.37.camel@kirk>*Sender*: huffman.brian.c at gmail.com

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. - Brian

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

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

- Previous by Date: Re: [isabelle] unicode tokens in isabelle2011+pg4.0
- Next by Date: [isabelle] String.explode in generated code
- 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