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



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.


	Makarius


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