[isabelle-dev] Mixfix-Syntax not recognized

René Neumann rene.neumann at in.tum.de
Wed Aug 7 11:02:58 CEST 2013

Am 06.08.2013 16:41, schrieb René Neumann:
> It is probably related to the thread "Subscripts within identifiers",
> but I'm not definitly sure.

Most definitly: This behavior has been introduced with rev 3ac2878764f9.

The question that remains (I could not grok it from the other thread):
Is it now completely forbidden to use superscripts (except for
esup-bsup) for such cases? Or can one only use non-letters (like the
aforementioned infinity)?

- René
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4782 bytes
Desc: S/MIME Kryptografische Unterschrift
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130807/d8a99119/attachment.bin>

More information about the isabelle-dev mailing list