Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] @{command and "fixes"


view this post on Zulip 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?

view this post on Zulip 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:

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: Mar 29 2024 at 12:28 UTC