[isabelle] @{command and "fixes"



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.