Re: [isabelle] document antiquotation for locale names

Hi Christian,

> I found the document antiquotation @{class c} for printing a class name
> (I guess). Is there a similar antiquotation for names of locales?

I don't think so.

> If not, how about adding one, just for completeness?

I would recommend to implement it first privately, a way which to some
extent even follows the Isabelle documentation itself (cf.
Doc/antiquote_setup.ML, which is a nice tutorial also).  There are a
couple of questions (e.g. what to refer to exactly?  locale names? locae
expressions?) which should be ironed out before such a thing becomes
official and thus making it harder to reshape it.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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