--- 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