*To*: Robert Lamar <rlamar at stetson.edu>*Subject*: Re: [isabelle] Conjunctions commutative in function arguments?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Thu, 2 Mar 2006 10:43:40 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <16530916C2FEF64EBE4C333390E3BEFC04FB5DF7@beta.ad.stetson.edu>*References*: <16530916C2FEF64EBE4C333390E3BEFC04FB5DF7@beta.ad.stetson.edu>

simp add: conj_commute Larry Paulson On 1 Mar 2006, at 21:24, Robert Lamar wrote:

Are there special considerations for conjunctions and other basic(or otherwise) logical operators when they are included asarguments to functions? Currently I am running into a wall on aproof that may be characterized by the failure of the folowingresult. The conjecturelemma "f ( P & Q ) ==> f ( Q & P )" will not be proved by simp, auto, or blast, but lemma "P & Q ==> Q & P" by auto is evaluated without complaint.Am I missing something basic? Any thoughts on this question wouldbe appreciated.

**References**:**[isabelle] Conjunctions commutative in function arguments?***From:*Robert Lamar

- Previous by Date: Re: [isabelle] Conjunctions commutative in function arguments?
- Next by Date: Re: [isabelle] Isabelle/Isar crash
- Previous by Thread: Re: [isabelle] Conjunctions commutative in function arguments?
- Next by Thread: Re: [isabelle] Conjunctions commutative in function arguments?
- Cl-isabelle-users March 2006 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