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)
 apply(auto)
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)"


--
DH




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