Re: [isabelle] Mistakes in Proving



On 14.10.2010 13:38, Viorel Preoteasa wrote:
lemma "P1(x) ==>  f1(x) \<in>  h1(w)"
   apply (rule C1);
   apply (rule B1);
   by simp;

Automating this proof is a different problem that I don't know how
to answer.

In this case it would by solved "by (auto intro: B1 C1).





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