diff -r 318acc1c9399 -r 30e6e070bdb6 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Sat Nov 07 08:17:52 2009 +0100
+++ b/src/HOL/Library/Sublist_Order.thy	Sat Nov 07 08:17:52 2009 +0100
@@ -226,8 +226,7 @@
 lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
 by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
 
-
-lemma "xs <= ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
+lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
 proof
   assume ?L
   thus ?R