# HG changeset patch
# User nipkow
# Date 1505409692 -7200
# Node ID 59acf5e73176393fcd34d900e3bd4a85f3597bde
# Parent  6f82e2ad261a08fffee1ed406b203772c3f8fdc4
two new simp rules

diff -r 6f82e2ad261a -r 59acf5e73176 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 14 17:36:06 2017 +0200
+++ b/src/HOL/List.thy	Thu Sep 14 19:21:32 2017 +0200
@@ -2014,11 +2014,17 @@
 
 subsubsection \<open>@{const take} and @{const drop}\<close>
 
-lemma take_0 [simp]: "take 0 xs = []"
+lemma take_0: "take 0 xs = []"
+by (induct xs) auto
+
+lemma drop_0: "drop 0 xs = xs"
 by (induct xs) auto
 
-lemma drop_0 [simp]: "drop 0 xs = xs"
-by (induct xs) auto
+lemma take0[simp]: "take 0 = (\<lambda>xs. [])"
+by(rule ext) (rule take_0)
+
+lemma drop0[simp]: "drop 0 = (\<lambda>x. x)"
+by(rule ext) (rule drop_0)
 
 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
 by simp