# Re: [isabelle] Proving formulae from separate sets of axioms

`This is not possible. In some cases it is possible to localize
``axioms by just making them assumptions of some lemmas. The locale
``mechanism (see locale tutorial) gives some tool support for doing
``this.
`

If I localise axioms, then would I be able to check whether r1 != r2?

`Checking r1 != r2 seems to need to look at *both* sets of axioms.
`

I meant that you could prove something like
"(Ax1 ==> f x = r1) ==> (Ax2 ==> f x = r2) ==> r1 = r2"

Also, can I check whether F is instantiated to the same thing on each
side?

`Not sure what you mean here with instantiated. If you have different
``descriptions of a function f, say "Ax1 f" and "Ax2 f", then the question
``can probably be expressed using the formula
`
"Ax1 f ==> Ax2 f' ==> f = f'"
Maybe you want to prove a statement like this.
Alex

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