changeset 68406 | 6beb45f6cf67 |
parent 67614 | 560fbd6bc047 |
child 71789 | 3b6547bdf6e2 |
--- a/src/HOL/Library/Sublist.thy Thu Jun 07 15:08:18 2018 +0200 +++ b/src/HOL/Library/Sublist.thy Thu Jun 07 19:36:12 2018 +0200 @@ -105,7 +105,7 @@ "prefix xs (ys @ zs) = (prefix xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefix us zs))" apply (induct zs rule: rev_induct) apply force - apply (simp del: append_assoc add: append_assoc [symmetric]) + apply (simp flip: append_assoc) apply (metis append_eq_appendI) done