How to write subscripts in Isabelle?

Question

How can one write subscripts in an Isabelle (2021) text command?

I tried to use the <^sub> symbol (which automatically converts to a down arrow) as follows:

text ‹
identity 1<^sub>S
›

but it gives an error:

Undefined document antiquotation: "sub"⌂

I also tried the LaTex way and used underscore _, but jEdit does not seem to recognize LaTex.

Answer 1

You can use the antiquotation text:

text ‹
identity \<^text>‹1⇩S›
›
(*or simply*)
text‹identity ‹1⇩S››

For further information about the command text see subsection 4.1 in the official documentation (The Isabelle/Isar Reference Manual or Isar-ref) of Isabelle2021, for further information about the antiquotation text see section 4.2 in the official documentation (Isar-ref) of Isabelle2021.

I also tried the LaTex way and used underscore _, but jEdit does not seem to recognize LaTex.

Further, please note that, in general, LaTeX output is generated while processing a session, and it is possible to augment theory files with arbitrary LaTeX source code like so:

text‹identity $1_S$›

In this case, $1_S$ should appear in the generated LaTeX documents, as expected. However, of course, jEdit will display this as raw LaTeX. For further information see the document The Isabelle/Isar Implementation (part of the official Isabelle2021 documentation) and, possibly, LaTeX Sugar for Isabelle Documents (also part of the official Isabelle2021 documentation).