[isabelle] Proving formulae from separate sets of axioms



Hi,

Can a formula describing the property a function should hold across
*several* theories? For example, I might have 2 theories T1.thy and T2.thy,
each with its own set of axioms. Can I prove something like there exists a
function F, variables x and y, such that F x y returns r1 in T1 and r2 in T2
and r1 != r2? T1 and T2 are each internally consistent, but together may be
inconsistent.

Thanks
Steve




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