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
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.)
"1.2.1 Strings of Symbols" for some explanations and specifications around
this important Isabelle concept.
This archive was generated by a fusion of
Pipermail (Mailman edition) and