Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] What characters are permitted in naming lemmas?

view this post on Zulip Email Gateway (Mar 03 2022 at 16:03):

From: Szymon Antoniak <sa394197@students.mimuw.edu.pl>
Hello,
I've got a very simple question: what is the alphabet of characters that one can use when naming objects like lemmas, definitions etc? Apologies if this is fundamental, but I was not able to find it in the reference manuals.

Szymon

view this post on Zulip Email Gateway (Mar 03 2022 at 16:33):

From: Dominique Unruh <unruh@ut.ee>
Hi,

I don't know the answer for sure, but you I think the list
letter_symbols in src/Pure/General/symbol.ML is an important part of
that alphabet.

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Mar 04 2022 at 10:29):

From: Makarius <makarius@sketis.net>
See also "isar-ref" manual, sections 3.2 and 3.3. But that is not the whole
story: as usual in Isabelle, everything is more complex as it seems.

Short story for end-users:

* Use double-quotes around fact names that don't fit into the regular
identifier model.

* Don't use non-identifiers for term names (variables etc.)

Makarius

Last updated: Jan 04 2025 at 20:18 UTC