doc-src/Tutorial/ToyList/lemma3
author ballarin
Fri, 02 May 2003 20:06:59 +0200
changeset 13950 74f638d8a829
parent 5377 efb799c5ed3c
permissions -rw-r--r--
File for document preparation.

Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
by(induct_tac "xs" 1);
by(Auto_tac);