Re: [isabelle] Access policy of qualified names [was: Theoryname.splits: Is this a feature?]
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