Make chunks_length a simp

HOL-Theorem-Prover · Dec 18, 2024 · 00b7c1d · 00b7c1d
1 parent b9dead1
commit 00b7c1d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
@@ -3217,7 +3217,7 @@ Proof
   \\ simp[]
 QED
 
-Theorem chunks_length:
+Theorem chunks_length[simp]:
   chunks (LENGTH ls) ls = [ls]
 Proof
   rw[Once chunks_def]