src/HOL/Library/Sublist.thy
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