Email Gateway (Aug 22 2022 at 12:38): Email Gateway (Aug 22 2022 at 12:38):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-December/msg00049.html
writes that the @{command antiquotation can be used via
ML_file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
However, \item @{command "fixes"} is not accepted by Isabelle2015.
Is "fixes" not a command in this sense, or just the above file is not ready for handling this case?
Email Gateway (Aug 22 2022 at 12:39):From: Makarius <makarius@sketis.net>
No it is a minor keyword, not a command keyword.
Isabelle2016 has various improvements to typeset Isar theory text, see
NEWS:
Antiquotation @{theory_text} prints uninterpreted theory source text
(Isar outer syntax with command keywords etc.). This may be used in the
short form \<^theory_text>\<open>...\<close>. @{theory_text [display]}
supports option "indent".
Antiquotations @{command}, @{method}, @{attribute} print checked
entities of the Isar language.
Which means the Isar antiquotations are there by default, but not needed
for quick informal snippets that should like like formal text.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC