src/HOL/Library/Sublist_Order.thy
changeset 33499 30e6e070bdb6
parent 33431 af516ed40e72
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/Library/Sublist_Order.thy	Sat Nov 07 08:17:52 2009 +0100
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Sat Nov 07 08:17:52 2009 +0100
     1.3 @@ -226,8 +226,7 @@
     1.4  lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
     1.5  by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
     1.6  
     1.7 -
     1.8 -lemma "xs <= ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
     1.9 +lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
    1.10  proof
    1.11    assume ?L
    1.12    thus ?R