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



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.