Re: [isabelle] Proofing across several theories

Stephy Wong wrote:
> Hi,
> 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?
> Thanks
> S
The only way one theory can refer to another is by importing it
(directly or indiectly), or by having a third theory that imports both.
You can qualify types etc from theory A by writing A.T.


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