*To*: Steve W <s.wong.731 at googlemail.com>*Subject*: Re: [isabelle] Proving formulae from separate sets of axioms*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Thu, 03 Sep 2009 10:39:42 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <12d162d00909021830h4891b3c5va6fee87b0554ee40@mail.gmail.com>*References*: <12d162d00909021830h4891b3c5va6fee87b0554ee40@mail.gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20090701)

Steve,

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.

Alex

**Follow-Ups**:**Re: [isabelle] Proving formulae from separate sets of axioms***From:*s . wong . 731

**References**:**[isabelle] Proving formulae from separate sets of axioms***From:*Steve W

- Previous by Date: [isabelle] Proving formulae from separate sets of axioms
- Next by Date: Re: [isabelle] Types for variables
- Previous by Thread: [isabelle] Proving formulae from separate sets of axioms
- 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