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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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