[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?

cheers

chris





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