| changeset 66891 | 5ec8cd4db7e2 |
| parent 66890 | e92d48a42a01 |
| child 66892 | d67d28254ff2 |
--- a/src/HOL/List.thy Sat Oct 21 18:14:59 2017 +0200 +++ b/src/HOL/List.thy Sat Oct 21 18:16:56 2017 +0200 @@ -2259,7 +2259,7 @@ finally show ?thesis . qed -lemma take_update_swap: "n < m \<Longrightarrow> take m (xs[n := x]) = (take m xs)[n := x]" +lemma take_update_swap: "take m (xs[n := x]) = (take m xs)[n := x]" apply(cases "n \<ge> length xs") apply simp apply(simp add: upd_conv_take_nth_drop take_Cons drop_take min_def diff_Suc