Re: [isabelle] subscripts in identifiers



On 8/22/2013 10:03 AM, Gergely Buday wrote:
Hi,

when will it be ready for the masses? In the next release?

- Gergely

Gergely,

You can already use subscripts within identifiers. The change is that superscripts in identifiers is going away, along with the \<^sub> and \<^sup> change.

http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg04431.html

http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg04418.html

What some people may not know, and which I learned recently is that theorem names can contain most anything, if you quote the theorem name. From one of the leading authorities on Isabelle:

   That is indeed a bit odd.  The normal way is to use "eq" as part of
   the name.  Apart from that, theorem names are not limited to
   identifiers at all, so if you put quotes around them, you may use
   whetever symbols you like, even a literal "=".

Regards,
GB



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