[isabelle] Proving theorems bridging between two theories/locales


I'm reposting a question from earlier:

I was wondering whether Isabelle can prove theorems bridging between two
theories or locales. For example, if I have A.thy and B.thy, can I prove
that there is a constant c in A that equals to v, while c in B that doesn't
equal to v? A and B can't be merged into one because together they'd be

Could locales be used here? It seems to me that: "locale C = A + B" would
merge A and B together to form C. Perhaps another operator could be used to
indicate that two locales are involved in the proof, but are not imported.
Is there a better way for proving bridging theorems? If not, would it
necessary for me to implement such an operator in ML? How much effort should
the implementation require?


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