[isabelle] record in a locale?

[Randy Pollack]

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

[Makarius]

On Sun, 19 May 2013, Randy Pollack wrote:

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

The record package is still not localized, so it is confined to old-style
global theory contexts. In principle it could be as local as 'typedef'
(i.e. with the same limitations), but it has not been done yet.

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

Logically, a local record definition cannot depend on context parameters /
premsises anyway, so the difference is again just one of name spaces etc.

You can pull your record definition in front of all your other definition,
and let it stand as global theory specification for now.


Makarius