src/HOL/List.thy

--- a/src/HOL/List.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/List.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -1526,7 +1526,7 @@
 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
 by (simp add: sublist_Cons)
 
-lemma sublist_upt_eq_take [simp]: "sublist l {..n(} = take n l"
+lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
 apply (induct l rule: rev_induct, simp)
 apply (simp split: nat_diff_split add: sublist_append)
 done