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