Re: [isabelle] HOLCF

On Wed, 27 Jun 2012, Christian Sternagel wrote:

* a space after the unicode symbol for "Lambda" is mandatory, otherwise we get an inner syntax error

This is a consequence of the way greek letters were added to the identifier syntax in 2003. \<lambda> was treated as a special case, and you loose in all other situations, such as \<Lambda> here, or \<mu>, \<iota> etc. that occurr occasionally in applications.

I have some ideas in the pipeline to address this problem and some others wrt. sub/superscripts within identifiers, but I did not manage to try that out yet, to see how it impacts existing theories. There is some renewed motivation to do it soon, because I don't want to imitate slightly odd identifier treatment of Proof General in Isabelle/jEdit.


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