src/HOL/Library/Sublist.thy
changeset 53015 a1119cf551e8
parent 52729 412c9e0381a1
child 54483 9f24325c2550
     1.1 --- a/src/HOL/Library/Sublist.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4    by (auto simp add: prefixeq_def)
     1.5  
     1.6  lemma prefixeq_same_cases:
     1.7 -  "prefixeq (xs\<^isub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^isub>2 ys \<Longrightarrow> prefixeq xs\<^isub>1 xs\<^isub>2 \<or> prefixeq xs\<^isub>2 xs\<^isub>1"
     1.8 +  "prefixeq (xs\<^sub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^sub>2 ys \<Longrightarrow> prefixeq xs\<^sub>1 xs\<^sub>2 \<or> prefixeq xs\<^sub>2 xs\<^sub>1"
     1.9    unfolding prefixeq_def by (metis append_eq_append_conv2)
    1.10  
    1.11  lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"