Re: [isabelle] Access policy of qualified names [was: Theoryname.splits: Is this a feature?]

Hi Nicole,

Most qualified names follow the default access policy. This is as follows: a qualified name x1.---.xn.y can be accessed by any suffix of the whole name, or by a prefix of x1.---.xn followed by y. Later accesses take priority over earlier ones.

You are probably right in pointing out that accesses of names generated by the datatype package (or by other packages) should always contain the name of the datatype. This would also disable to refer by "splits" to the splitting lemmas of the last datatype. I believe this hasn't been considered a problem since traditionally theory names are upper case while type names are lower.


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