Jakub Kądziołka (Mar 18 2021 at 23:59): Jakub Kądziołka (Mar 18 2021 at 23:59):I would like to introduce the constant that's about to be defined in my text. I'd rather make sure that the name in the text matches the actual name, so I want to use the @{const} antiquotation. However, this doesn't work, because the definition is below the text. Is there any workaround?
I'd also like to be able to give an example with @{lemma}, but it suffers from the same problem.
Of course, I could move the description below the definition, but I would really rather avoid that, as that's opposite of the natural reading order.
Lukas Stevens (Mar 19 2021 at 12:26):I think that is just not possible with Isabelle's document model. It is monotone. You can write the name of the definition in cartouches to approximate the behaviour.
Last updated: Dec 21 2024 at 16:20 UTC