Email Gateway (Aug 19 2022 at 16:48): Email Gateway (Aug 19 2022 at 16:48):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
I see that in Isabelle's documentation sources @{command ...} is used
quite frequently.
Any specific reasons why this antiquotation is not available inside
"normal" theories? Is there a way to make it available?
I think it is not completely uncommon that user-code introduces new
commands. In that cases @{command ...} would come in handy.
cheers
chris
Email Gateway (Aug 19 2022 at 16:48):From: Makarius <makarius@sketis.net>
It started out as a slightly adhoc thing just for the isar-ref manual, but
has become more important elsewhere over the years. Moving such things
into official space always requires some more work, but it is likely to
happen eventually.
Right now you can use it unofficially via
$ISABELLE_HOME/src/Doc/antiquote_setup.ML
Makarius
http://stop-ttip.org 1,103,194 people so far
Last updated: Apr 20 2024 at 08:16 UTC