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

On Wed, 2 Feb 2011, John Wickerson wrote:

Perhaps the fault lies not with PG but with Isabelle, for requiring the forall symbol to be inputted as \<forall> not as the unicode character ∀

This behaviour is according to the specification of Isabelle symbols. It has been there for so many years that 5 new unicode encodings have been invented in the meantime. I have also refined the whole concept of symbols and potential mappings wrt. external unicode recently for Isabelle/Scala, with quite detailed specifications in the Isabelle/Isar implementation manual.

You cannot expect that ancient Proof General 3.7.x fully complies with all that. I don't know about the exact behaviour of Proof General 4.1 either, which is still to be released. (This also means you can contribute to its issue tracker


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