author | wenzelm |
Mon, 26 Apr 2004 14:56:18 +0200 | |
changeset 14674 | 3506a9af46fc |
parent 5377 | efb799c5ed3c |
permissions | -rw-r--r-- |
Goal "xs @ [] = xs"; by(induct_tac "xs" 1); by(Auto_tac); qed "app_Nil2"; Addsimps [app_Nil2]; Goal "(xs @ ys) @ zs = xs @ (ys @ zs)"; by(induct_tac "xs" 1); by(Auto_tac); qed "app_assoc"; Addsimps [app_assoc]; Goal "rev(xs @ ys) = (rev ys) @ (rev xs)"; by(induct_tac "xs" 1); by(Auto_tac); qed "rev_app"; Addsimps [rev_app]; Goal "rev(rev xs) = xs"; by(induct_tac "xs" 1); by(Auto_tac); qed "rev_rev";