summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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