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 http://proofgeneral.inf.ed.ac.uk/trac/.)


	Makarius


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