From: "Vromen, H.J. (Huub)" <H.Vromen@ftr.ru.nl>
If A is a list, then I can refer to the nth element of the list by "nth A" or "A!n". But I would prefer to use "An" with a subscripted n, like usually is done in mathematics. Is this possible?
Huub Vromen
Radboud University-Nijmegen
Department of Philosophy
Room E 16.11
Erasmusplein 1
6525 HT Nijmegen
Netherlands
From: Tobias Nipkow <nipkow@in.tum.de>
If you are interested in generating nice latex/pdf outpout with that syntax:
In HOL/Library/LaTeXsugar.thy you find almost what you want:
(* nth *)
notation (latex output)
nth ("_\<^latex>‹\\ensuremath{_{[\\mathit{›_\<^latex>‹}]}}›" [1000,0] 1000)
Just remove the square brackets. This theory is full of other nice notational
tricks. The documentation for this theory is included in the list of documents
under the Documentation rider in Isabelle/jedit.
Tobias
smime.p7s
Last updated: May 04 2024 at 12:26 UTC