Re: [isabelle] record in a locale?
On Sun, 19 May 2013, Randy Pollack wrote:
Is it correct that you cannot define a record in the context of a
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and