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

Thanks,
Randy




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