[isabelle] record in a locale?

Is it correct that you cannot define a record in the context of a locale?

If so, is there a commonly used work around that is not so verbose as
nested products?


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