# HG changeset patch
# User nipkow
# Date 1731793593 -3600
# Node ID 42b0f923fd82ae27fe96882f523c2119fa8a8ed2
# Parent  2575f1bd226be0e976633686b2e6a087292336de
tuned

diff -r 2575f1bd226b -r 42b0f923fd82 src/HOL/Data_Structures/Selection.thy
--- a/src/HOL/Data_Structures/Selection.thy	Sat Nov 16 21:36:34 2024 +0100
+++ b/src/HOL/Data_Structures/Selection.thy	Sat Nov 16 22:46:33 2024 +0100
@@ -126,6 +126,7 @@
 | "chop n xs = take n xs # chop n (drop n xs)"
 
 lemmas [simp del] = chop.simps
+lemmas [simp] = chop.simps(1)
 
 text \<open>
   This is an alternative induction rule for \<^const>\<open>chop\<close>, which is often nicer to use.
@@ -143,11 +144,8 @@
 lemma chop_eq_Nil_iff [simp]: "chop n xs = [] \<longleftrightarrow> n = 0 \<or> xs = []"
   by (induction n xs rule: chop.induct; subst chop.simps) auto
 
-lemma chop_0 [simp]: "chop 0 xs = []"
-  by (simp add: chop.simps)
-
 lemma chop_Nil [simp]: "chop n [] = []"
-  by (cases n) (auto simp: chop.simps)
+  by (cases n) auto
 
 lemma chop_reduce: "n > 0 \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> chop n xs = take n xs # chop n (drop n xs)"
   by (cases n; cases xs) (auto simp: chop.simps)