# HG changeset patch
# User haftmann
# Date 1274369702 -7200
# Node ID a6e0696d7110e1ab7b1d8819d31ad09388f796be
# Parent  98bfff1d159d228ca7f161a0bacb256552e319fc
proper document text

diff -r 98bfff1d159d -r a6e0696d7110 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Thu May 20 17:29:43 2010 +0200
+++ b/src/HOL/Library/More_List.thy	Thu May 20 17:35:02 2010 +0200
@@ -237,7 +237,7 @@
   "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map ..
 
-text {* nth_map *}
+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