# HG changeset patch
# User haftmann
# Date 1325844902 -3600
# Node ID 94479a979129fd3ea57dcd2dd9947733f31d6a14
# Parent  ab21fc844ea260d2605f3bf8d419b7238c3ef4c5
dropped unused nth_map

diff -r ab21fc844ea2 -r 94479a979129 src/HOL/More_List.thy
--- a/src/HOL/More_List.thy	Fri Jan 06 10:53:52 2012 +0100
+++ b/src/HOL/More_List.thy	Fri Jan 06 11:15:02 2012 +0100
@@ -6,34 +6,6 @@
 imports List
 begin
 
-text {* @{text nth_map} *}
-
-definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "nth_map n f xs = (if n < length xs then
-       take n xs @ [f (xs ! n)] @ drop (Suc n) xs
-     else xs)"
-
-lemma nth_map_id:
-  "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
-  by (simp add: nth_map_def)
-
-lemma nth_map_unfold:
-  "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
-  by (simp add: nth_map_def)
-
-lemma nth_map_Nil [simp]:
-  "nth_map n f [] = []"
-  by (simp add: nth_map_def)
-
-lemma nth_map_zero [simp]:
-  "nth_map 0 f (x # xs) = f x # xs"
-  by (simp add: nth_map_def)
-
-lemma nth_map_Suc [simp]:
-  "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
-  by (simp add: nth_map_def)
-
-
 text {* monad operation *}
 
 definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where