Email Gateway (Aug 22 2022 at 20:24): Email Gateway (Aug 22 2022 at 20:24):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
Email Gateway (Aug 22 2022 at 20:24):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: Apr 25 2024 at 04:18 UTC