*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Proving formulae from separate sets of axioms*From*: Steve W <s.wong.731 at googlemail.com>*Date*: Thu, 3 Sep 2009 02:30:25 +0100

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

**Follow-Ups**:**Re: [isabelle] Proving formulae from separate sets of axioms***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Obtaining the instantiation of variables in a proof
- Next by Date: Re: [isabelle] Proving formulae from separate sets of axioms
- Previous by Thread: Re: [isabelle] Obtaining the instantiation of variables in a proof
- Next by Thread: Re: [isabelle] Proving formulae from separate sets of axioms
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list