Re: [isabelle] proof solution [ newbie question ]



Since my original lemma said "hd xs = c and hd ys = c" I wrongly assumed
that this implied that xs and ys were non-empty. The neq_Nil_conv lemma
worked well for this proof. Also, the cases method answered a question I had
about another proof.

Thanks!
Greg




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