# [isabelle] @{command and "fixes"

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?

- Gergely

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.