diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -68,7 +68,7 @@
   have "inj_on nat (abs ` A)" for A
     by (rule inj_onI) auto
   then show ?thesis
-    by (auto simp add: image_comp [symmetric] dest: finite_image_absD finite_imageD)
+    by (auto simp flip: image_comp dest: finite_image_absD finite_imageD)
 qed
 
 proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
@@ -161,11 +161,11 @@
 
 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
   for P :: "nat \<Rightarrow> bool"
-  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
+  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq simp flip: not_le)
 
 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
   for P :: "nat \<Rightarrow> bool"
-  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
+  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq simp flip: not_le)
 
 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
   for P :: "nat \<Rightarrow> bool"
@@ -286,7 +286,7 @@
     apply (subst Suc)
      apply (use \<open>infinite S\<close> in simp)
     apply (intro arg_cong[where f = Least] ext)
-    apply (auto simp: enumerate_Suc'[symmetric])
+    apply (auto simp flip: enumerate_Suc')
     done
 qed