Email Gateway (Aug 19 2022 at 11:41): Email Gateway (Aug 19 2022 at 11:41):From: Gergely Buday <gbuday@gmail.com>
Hi,
when will it be ready for the masses? In the next release?
Email Gateway (Aug 19 2022 at 11:41):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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@mailbroy.informatik.tu-muenchen.de/msg04431.html
http://www.mail-archive.com/isabelle-dev@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
Last updated: Apr 20 2024 at 08:16 UTC