Charles Staats (Mar 21 2023 at 20:36): Charles Staats (Mar 21 2023 at 20:36):I find myself wanting to write things like "In this section the <locale name> is defined." or "The following definition will allow us to write <notation example>."
It is very important to me for the sake of good exposition that in certain cases, a rough explanation should come before the thing being defined.
Unfortunately the naive approach (unsurprisingly) gives errors when I try it this way. How do I make it work? Do I just need to use standard TeX symbols instead of antiquotations, or is there a better way?
Lukas Stevens (Mar 21 2023 at 22:27):Forward references go against the document model of Isabelle. What is your use case? Do you want to document the theory on the fly or are you writing a paper?
Wolfgang Jeltsch (Mar 22 2023 at 12:43):There are the generic antiquotation types text (for inner syntax) and theory_text (for outer syntax). In the standard configuration. For inner syntax, it is also possible to just put your text into cartouches. Of course, with these constructs, you only get basic checks (just the syntax is checked, from what I remember).
Last updated: Apr 26 2024 at 08:19 UTC