[isabelle] document antiquotation for locale names

Dear all,

I found the document antiquotation @{class c} for printing a class name (I guess). Is there a similar antiquotation for names of locales? If not, how about adding one, just for completeness?



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