# HG changeset patch
# User paulson
# Date 1136809664 -3600
# Node ID 4524643feecc47cc4024cce53e5523d51cde91ab
# Parent  4a3806b41d29361b72c331205f3307b038ab90ab
theorems need names

diff -r 4a3806b41d29 -r 4524643feecc src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jan 09 00:05:10 2006 +0100
+++ b/src/HOL/List.thy	Mon Jan 09 13:27:44 2006 +0100
@@ -1728,9 +1728,13 @@
 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
 by (cases n) simp_all
 
-lemmas [simp] = take_Cons'[of "number_of v",standard]
-                drop_Cons'[of "number_of v",standard]
-                nth_Cons'[of _ _ "number_of v",standard]
+lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
+lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
+lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
+
+declare take_Cons_number_of [simp] 
+        drop_Cons_number_of [simp] 
+        nth_Cons_number_of [simp] 
 
 
 subsubsection {* @{text "distinct"} and @{text remdups} *}