[isabelle] antiquotation @{command ...}

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.



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