Would you expect something like this to work?
lemma conj_commute: "P & Q ==> Q & P" by auto
lemma "f ( P & Q ) ==> f ( Q & P )"
proof 
assume "f( P & Q )"
from this conj_commute [of P Q]
have "f( Q & P )" by simp
qed
This is less terse, but it is more similar to the methods I am using in my proof. It fails as well, I am afraid.
Robert Lamar
On Thu 3/2/2006 5:43 AM, Larry Paulson wrote:

 The lemma "conj_commute" expresses commutativity of the conjunction
 operator. You should be able to prove your theorem with something like

 simp add: conj_commute

 Larry Paulson
