[isabelle] Proofing across several theories


I was wondering whether one could proof a goal across several separate
theories. For example, given two theories a.thy and b.thy, can a goal like
\exists t:T, q:Q.t -> q in a.thy and \exists t:T, p:P. t -> p, where T and P
are types, be proven. Here, I want T to be the same in both theories. Can
this information be passed from one theory to another? If so, since a.thy
and b.thy are separate, can they be inconsistent with each other?



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