Re: [isabelle] subscripts in identifiers
On 8/22/2013 10:03 AM, Gergely Buday wrote:
when will it be ready for the masses? In the next release?
You can already use subscripts within identifiers. The change is that
superscripts in identifiers is going away, along with the \<^sub> and
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 "=".
This archive was generated by a fusion of
Pipermail (Mailman edition) and