--- a/src/HOL/Library/Sublist.thy Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Library/Sublist.thy Sun Nov 26 21:08:32 2017 +0100
@@ -1018,7 +1018,7 @@
"subseq (xs @ zs) (ys @ zs) \<longleftrightarrow> subseq xs ys" (is "?l = ?r")
proof
{ fix xs' ys' xs ys zs :: "'a list" assume "subseq xs' ys'"
- then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> subseq xs ys"
+ then have "xs' = xs @ zs \<and> ys' = ys @ zs \<longrightarrow> subseq xs ys"
proof (induct arbitrary: xs ys zs)
case list_emb_Nil show ?case by simp
next