Re: [isabelle] [Noob] Proof on trees

Played about with it a bit, and the following went through OK:

lemma "(dfs1 xs)@list  = dfs2 xs list"
 apply(induction xs arbitrary:list)
by (metis Cons_eq_appendI append_assoc)

induction is a newer method than induct_tac, though I don't know the details. Once I'd changed that, sledgehammer came up with the.."by (metis Cons_eq_appendI append_assoc)"


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