# [isabelle] Proving theorems bridging between two theories/locales

Hi,
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
inconsistent.
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?
Thanks
Steve

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