src/HOL/Library/Sublist.thy
changeset 61076 bdc1e2f0a86a
parent 60679 ade12ef2773c
child 63117 acb6d72fc42e
     1.1 --- a/src/HOL/Library/Sublist.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4      assume a1: "\<exists>zs. ys = xs @ zs"
     1.5      then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
     1.6      assume a2: "length xs < length ys"
     1.7 -    have f1: "\<And>v. ([]\<Colon>'a list) @ v = v" using append_Nil2 by simp
     1.8 +    have f1: "\<And>v. ([]::'a list) @ v = v" using append_Nil2 by simp
     1.9      have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
    1.10      hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
    1.11      thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce