Re: [isabelle] Proofing across several theories
Stephy Wong wrote:
> 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?
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