Re: [isabelle] Record field names and accessing other constants
You can refer to all constants with their unique long name (unless
access has been disabled explicitly with hide_const). In your example,
you can refer to y introduced in the consts declaration as TheoryName.y
where TheoryName is the name of the theory that contains the
declaration. Side remark: Name hiding is not specific to the record package.
On 02/08/2013 08:53 PM, Yannick Duchêne (Hibou57) wrote:
A sample case:
consts y :: bool
consts z :: bool
record u = x :: bool
record v = x :: bool y :: bool
term "(| u.x = y |)"
term "(| v.x = y, v.y = y |)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and