# HG changeset patch
# User nipkow
# Date 1020072574 -7200
# Node ID 04f8cbd1b500ce59a1e1e41856f2c886c53885e3
# Parent  8ed413a57bdcec8045db7b025401157907ae1de3
added rev_take and rev_drop

diff -r 8ed413a57bdc -r 04f8cbd1b500 src/HOL/List.ML
--- 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;