[isabelle] a little problem



Dear friends,

 

I have a promble about verifying the next lemma.

 

lemma add_finite : "finite A \<and> A \<noteq> {} \<Longrightarrow> finite {(x::nat) + m |m. m \<in> A}" 

 

Need your help! Thanks.

                                                                          yucy


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