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

Makarius wrote:
notation (input) All (binder "∀" 10)

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

Are you saying that the Unicode code points listed in $ISABELLE_HOME/etc/symbols may not occur regularly in the sources? The section in the implementation manual does not make this clear... In fact what I read there is that any UTF-8 sequence is legal. So then it should not be a problem to declare the ab

Or is it an additional constraint imposed by the jEdit layer? PG 4 seems to differentiate between the different classes of symbols...


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