--- a/src/HOL/List.ML Fri Apr 26 11:47:01 2002 +0200
+++ b/src/HOL/List.ML Mon Apr 29 11:29:34 2002 +0200
@@ -896,6 +896,20 @@
by Auto_tac;
qed_spec_mp "drop_map";
+Goal "!i. rev (take i xs) = drop (length xs - i) (rev xs)";
+by(induct_tac "xs" 1);
+ by Auto_tac;
+by (case_tac "i" 1);
+ by Auto_tac;
+qed_spec_mp "rev_take";
+
+Goal "!i. rev (drop i xs) = take (length xs - i) (rev xs)";
+by(induct_tac "xs" 1);
+ by Auto_tac;
+by (case_tac "i" 1);
+ by Auto_tac;
+qed_spec_mp "rev_drop";
+
Goal "!n i. i < n --> (take n xs)!i = xs!i";
by (induct_tac "xs" 1);
by Auto_tac;