author | wenzelm |
Wed, 13 Oct 1999 19:42:12 +0200 | |
changeset 7854 | fe7b7e3c3ddc |
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";