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

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to