Re: [isabelle] Conjunctions commutative in function arguments?



    lemma conj_commute: "P & Q ==> Q & P" by auto

is not a very useful lemma in your context. It is just not true that "A ==>
B" implies "f A ==> f B", sorry. If you replace "==>" by "=" it becomes
true. Hence the popularity of "=", one of the greatest inventions of
mathematics.

Tobias





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