src/HOL/Imperative_HOL/ex/Sublist.thy
changeset 53374 a14d2a854c02
parent 45129 1fce03e3e8ad
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -490,7 +490,6 @@
     1.4    moreover
     1.5    from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
     1.6      by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
     1.7 -  moreover
     1.8    ultimately show ?thesis by (simp add: multiset_of_append)
     1.9  qed
    1.10