Re: [isabelle] antiquotation @{command ...}

On Tue, 9 Dec 2014, Christian Sternagel wrote:

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.

It started out as a slightly adhoc thing just for the isar-ref manual, but has become more important elsewhere over the years. Moving such things into official space always requires some more work, but it is likely to happen eventually.

Right now you can use it unofficially via $ISABELLE_HOME/src/Doc/antiquote_setup.ML


           1,103,194 people so far

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