# HG changeset patch
# User nipkow
# Date 1528392972 -7200
# Node ID 6beb45f6cf67e3a3cdb09607c79245b2b9f4c1e3
# Parent  6a0852b8e5a8cff58a00a9e6e24724051c7d051b
utilize 'flip'

diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/BigO.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -188,7 +188,7 @@
   apply (rule_tac x = "\<bar>c\<bar>" in exI)
   apply auto
   apply (drule_tac x = x in spec)+
-  apply (simp add: abs_mult [symmetric])
+  apply (simp flip: abs_mult)
   done
 
 lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)"
@@ -271,7 +271,7 @@
   also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
     by (rule bigo_plus_eq, auto)
   finally show ?thesis
-    by (simp add: bigo_abs3 [symmetric])
+    by (simp flip: bigo_abs3)
 qed
 
 lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"
@@ -447,7 +447,7 @@
   for c :: "'a::linordered_field"
   apply (simp add: bigo_def)
   apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
-  apply (simp add: abs_mult [symmetric])
+  apply (simp flip: abs_mult)
   done
 
 lemma bigo_const4: "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"
@@ -468,7 +468,7 @@
 lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
   apply (simp add: bigo_def)
   apply (rule_tac x = "\<bar>c\<bar>" in exI)
-  apply (auto simp add: abs_mult [symmetric])
+  apply (auto simp flip: abs_mult)
   done
 
 lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Cardinality.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -62,7 +62,7 @@
 by(simp add: card_UNIV_option)
 
 lemma card_UNIV_set: "CARD('a set) = (if CARD('a) = 0 then 0 else 2 ^ CARD('a))"
-by(simp add: Pow_UNIV[symmetric] card_eq_0_iff card_Pow del: Pow_UNIV)
+by(simp add: card_eq_0_iff card_Pow flip: Pow_UNIV)
 
 lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
 by(simp add: card_UNIV_set)
@@ -267,7 +267,7 @@
 definition "finite_UNIV = Phantom('a + 'b)
   (of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))"
 instance
-  by intro_classes (simp add: UNIV_Plus_UNIV[symmetric] finite_UNIV_sum_def finite_UNIV del: UNIV_Plus_UNIV)
+  by intro_classes (simp add: finite_UNIV_sum_def finite_UNIV)
 end
 
 instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Countable.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -101,8 +101,8 @@
 
 qualified termination
 by (relation "measure id")
-  (auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
-    le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
+  (auto simp flip: sum_encode_eq prod_encode_eq
+    simp: le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
     le_prod_encode_1 le_prod_encode_2)
 
 lemma nth_item_covers: "finite_item x \<Longrightarrow> \<exists>n. nth_item n = x"
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -125,7 +125,7 @@
 proof -
   have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
     by transfer_prover
-  then show ?thesis by (simp add: cUnion_def [symmetric])
+  then show ?thesis by (simp flip: cUnion_def)
 qed
 
 lemmas cset_eqI = set_eqI[Transfer.transferred]
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -55,7 +55,7 @@
   moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
   ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
     using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
-    by (auto simp: INT_Int_distrib[symmetric])
+    by (auto simp flip: INT_Int_distrib)
 qed
 
 subsubsection "Family of Disjoint Sets"
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -321,7 +321,7 @@
   by (simp add: eSuc_def split: enat.split)
 
 lemma eSuc_minus_1 [simp]: "eSuc n - 1 = n"
-  by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric])
+  by (simp add: one_enat_def flip: eSuc_enat zero_enat_def)
 
 (*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
 
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -486,10 +486,10 @@
   by transfer (simp add: top_ereal_def)
 
 lemma ennreal_top_neq_one[simp]: "top \<noteq> (1::ennreal)"
-  by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
+  by transfer (simp add: top_ereal_def one_ereal_def flip: ereal_max)
 
 lemma ennreal_one_neq_top[simp]: "1 \<noteq> (top::ennreal)"
-  by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
+  by transfer (simp add: top_ereal_def one_ereal_def flip: ereal_max)
 
 lemma ennreal_add_less_top[simp]:
   fixes a b :: ennreal
@@ -636,7 +636,7 @@
   apply transfer
   subgoal for a b c
     apply (cases a b c rule: ereal3_cases)
-    apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
+    apply (auto simp flip: ereal_max)
     done
   done
 
@@ -654,7 +654,7 @@
   unfolding divide_ennreal_def
   apply transfer
   apply (subst mult.assoc)
-  apply (simp add: top_ereal_def divide_ereal_def[symmetric])
+  apply (simp add: top_ereal_def flip: divide_ereal_def)
   done
 
 lemma divide_mult_eq: "a \<noteq> 0 \<Longrightarrow> a \<noteq> \<infinity> \<Longrightarrow> x * a / (b * a) = x / (b::ennreal)"
@@ -672,7 +672,7 @@
   unfolding divide_ennreal_def
   apply transfer
   apply (subst mult.assoc)
-  apply (simp add: top_ereal_def divide_ereal_def[symmetric])
+  apply (simp add: top_ereal_def flip: divide_ereal_def)
   done
 
 lemma ennreal_add_diff_cancel:
@@ -686,7 +686,7 @@
   apply transfer
   subgoal for a b
     apply (cases a b rule: ereal2_cases)
-    apply (auto simp: zero_ereal_def ereal_max[symmetric] max.absorb2 simp del: ereal_max)
+    apply (auto simp: zero_ereal_def max.absorb2 simp flip: ereal_max)
     done
   done
 
@@ -859,7 +859,7 @@
 lemmas ennreal3_cases = ennreal_cases[case_product ennreal2_cases]
 
 lemma ennreal_neq_top[simp]: "ennreal r \<noteq> top"
-  by transfer (simp add: top_ereal_def zero_ereal_def ereal_max[symmetric] del: ereal_max)
+  by transfer (simp add: top_ereal_def zero_ereal_def flip: ereal_max)
 
 lemma top_neq_ennreal[simp]: "top \<noteq> ennreal r"
   using ennreal_neq_top[of r] by (auto simp del: ennreal_neq_top)
@@ -920,16 +920,13 @@
   by (cases "0 \<le> y") (auto simp: ennreal_eq_0_iff ennreal_neg)
 
 lemma ennreal_eq_1[simp]: "ennreal x = 1 \<longleftrightarrow> x = 1"
-  by (cases "0 \<le> x")
-     (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
+  by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
 
 lemma ennreal_le_1[simp]: "ennreal x \<le> 1 \<longleftrightarrow> x \<le> 1"
-  by (cases "0 \<le> x")
-     (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
+  by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
 
 lemma ennreal_ge_1[simp]: "ennreal x \<ge> 1 \<longleftrightarrow> x \<ge> 1"
-  by (cases "0 \<le> x")
-     (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
+  by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
 
 lemma one_less_ennreal[simp]: "1 < ennreal x \<longleftrightarrow> 1 < x"
   by transfer (auto simp: max.absorb2 less_max_iff_disj)
@@ -977,7 +974,7 @@
 
 lemma ennreal_minus: "0 \<le> q \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
   by transfer
-     (simp add: max.absorb2 zero_ereal_def ereal_max[symmetric] del: ereal_max)
+     (simp add: max.absorb2 zero_ereal_def flip: ereal_max)
 
 lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
   by (simp add: minus_top_ennreal)
@@ -1050,8 +1047,7 @@
   "(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
   apply (cases y rule: ennreal_cases)
   apply (cases x rule: ennreal_cases)
-  apply (auto simp del: ennreal_plus simp add: top_unique ennreal_plus[symmetric]
-    intro: zero_less_one field_le_epsilon)
+  apply (auto simp flip: ennreal_plus simp add: top_unique intro: zero_less_one field_le_epsilon)
   done
 
 lemma ennreal_rat_dense:
@@ -1394,7 +1390,7 @@
 
 lemma ennreal_suminf_neq_top: "summable f \<Longrightarrow> (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top"
   using sums_ennreal[of f "suminf f"]
-  by (simp add: suminf_nonneg sums_unique[symmetric] summable_sums_iff[symmetric] del: sums_ennreal)
+  by (simp add: suminf_nonneg flip: sums_unique summable_sums_iff del: sums_ennreal)
 
 lemma suminf_ennreal_eq:
   "(\<And>i. 0 \<le> f i) \<Longrightarrow> f sums x \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal x"
@@ -1598,7 +1594,7 @@
   apply transfer
   subgoal for A
     using Inf_countable_INF[of A]
-    apply (clarsimp simp add: decseq_def[symmetric])
+    apply (clarsimp simp flip: decseq_def)
     subgoal for f
       by (intro exI[of _ f]) auto
     done
@@ -1794,19 +1790,17 @@
 by (auto simp: top_unique)
 
 lemma diff_diff_ennreal: fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> b - (b - a) = a"
-  by (cases a b rule: ennreal2_cases)
-     (auto simp: ennreal_minus top_unique)
+  by (cases a b rule: ennreal2_cases) (auto simp: ennreal_minus top_unique)
 
 lemma ennreal_less_one_iff[simp]: "ennreal x < 1 \<longleftrightarrow> x < 1"
-  by (cases "0 \<le> x")
-     (auto simp: ennreal_neg ennreal_1[symmetric] ennreal_less_iff simp del: ennreal_1)
+  by (cases "0 \<le> x") (auto simp: ennreal_neg ennreal_less_iff simp flip: ennreal_1)
 
 lemma SUP_const_minus_ennreal:
   fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
   including ennreal.lifting
   by (transfer fixing: I)
-     (simp add: sup_ereal_def[symmetric] SUP_sup_distrib[symmetric] SUP_ereal_minus_right
-           del: sup_ereal_def)
+     (simp add: SUP_sup_distrib[symmetric] SUP_ereal_minus_right
+           flip: sup_ereal_def)
 
 lemma zero_minus_ennreal[simp]: "0 - (a::ennreal) = 0"
   including ennreal.lifting
@@ -1846,10 +1840,8 @@
 lemma add_diff_le_ennreal: "a + b - c \<le> a + (b - c::ennreal)"
   apply (cases a b c rule: ennreal3_cases)
   subgoal for a' b' c'
-    by (cases "0 \<le> b' - c'")
-       (simp_all add: ennreal_minus ennreal_plus[symmetric] top_add ennreal_neg
-                 del: ennreal_plus)
-  apply (simp_all add: top_add ennreal_plus[symmetric] del: ennreal_plus)
+    by (cases "0 \<le> b' - c'") (simp_all add: ennreal_minus top_add ennreal_neg flip: ennreal_plus)
+  apply (simp_all add: top_add flip: ennreal_plus)
   done
 
 lemma diff_eq_0_ennreal: "a < top \<Longrightarrow> a \<le> b \<Longrightarrow> a - b = (0::ennreal)"
@@ -1857,14 +1849,14 @@
 
 lemma diff_diff_ennreal': fixes x y z :: ennreal shows "z \<le> y \<Longrightarrow> y - z \<le> x \<Longrightarrow> x - (y - z) = x + z - y"
   by (cases x; cases y; cases z)
-     (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique
-           simp del: ennreal_plus)
+     (auto simp add: top_add add_top minus_top_ennreal ennreal_minus top_unique
+           simp flip: ennreal_plus)
 
 lemma diff_diff_ennreal'': fixes x y z :: ennreal
   shows "z \<le> y \<Longrightarrow> x - (y - z) = (if y - z \<le> x then x + z - y else 0)"
   by (cases x; cases y; cases z)
-     (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique ennreal_neg
-           simp del: ennreal_plus)
+     (auto simp add: top_add add_top minus_top_ennreal ennreal_minus top_unique ennreal_neg
+           simp flip: ennreal_plus)
 
 lemma power_less_top_ennreal: fixes x :: ennreal shows "x ^ n < top \<longleftrightarrow> x < top \<or> n = 0"
   using power_eq_top_ennreal[of x n] by (auto simp: less_top)
@@ -1880,7 +1872,7 @@
      (auto simp: divide_ennreal ennreal_mult[symmetric] ennreal_less_iff field_simps ennreal_top_mult ennreal_top_divide)
 
 lemma one_less_numeral[simp]: "1 < (numeral n::ennreal) \<longleftrightarrow> (num.One < n)"
-  by (simp del: ennreal_1 ennreal_numeral add: ennreal_1[symmetric] ennreal_numeral[symmetric] ennreal_less_iff)
+  by (simp flip: ennreal_1 ennreal_numeral add: ennreal_less_iff)
 
 lemma divide_eq_1_ennreal: "a / b = (1::ennreal) \<longleftrightarrow> (b \<noteq> top \<and> b \<noteq> 0 \<and> b = a)"
   by (cases a ; cases b; cases "b = 0") (auto simp: ennreal_top_divide divide_ennreal split: if_split_asm)
@@ -1902,17 +1894,16 @@
 
 lemma ennreal_minus_le_iff: "a - b \<le> c \<longleftrightarrow> (a \<le> b + (c::ennreal) \<and> (a = top \<and> b = top \<longrightarrow> c = top))"
   by (cases a; cases b; cases c)
-     (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric]
-           simp del: ennreal_plus)
+     (auto simp: top_unique top_add add_top ennreal_minus simp flip: ennreal_plus)
 
 lemma ennreal_le_minus_iff: "a \<le> b - c \<longleftrightarrow> (a + c \<le> (b::ennreal) \<or> (a = 0 \<and> b \<le> c))"
   by (cases a; cases b; cases c)
-     (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric] ennreal_le_iff2
-           simp del: ennreal_plus)
+     (auto simp: top_unique top_add add_top ennreal_minus ennreal_le_iff2
+           simp flip: ennreal_plus)
 
 lemma diff_add_eq_diff_diff_swap_ennreal: "x - (y + z :: ennreal) = x - y - z"
   by (cases x; cases y; cases z)
-     (auto simp: ennreal_plus[symmetric] ennreal_minus_if add_top top_add simp del: ennreal_plus)
+     (auto simp: ennreal_minus_if add_top top_add simp flip: ennreal_plus)
 
 lemma diff_add_assoc2_ennreal: "b \<le> a \<Longrightarrow> (a - b + c::ennreal) = a + c - b"
   by (cases a; cases b; cases c)
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -174,7 +174,7 @@
     then obtain n m where "{enat n<..} \<subseteq> A" "{enat m<..} \<subseteq> B"
       by auto
     then have "{enat (max n m) <..} \<subseteq> A \<inter> B"
-      by (auto simp add: subset_eq Ball_def max_def enat_ord_code(1)[symmetric] simp del: enat_ord_code(1))
+      by (auto simp add: subset_eq Ball_def max_def simp flip: enat_ord_code(1))
     then show ?case
       by auto
   next
@@ -415,7 +415,7 @@
 
 lemma ereal_0_plus [simp]: "ereal 0 + x = x"
   and plus_ereal_0 [simp]: "x + ereal 0 = x"
-by(simp_all add: zero_ereal_def[symmetric])
+by(simp_all flip: zero_ereal_def)
 
 instance ereal :: numeral ..
 
@@ -939,7 +939,7 @@
 lemma [simp]:
   shows ereal_1_times: "ereal 1 * x = x"
   and times_ereal_1: "x * ereal 1 = x"
-by(simp_all add: one_ereal_def[symmetric])
+by(simp_all flip: one_ereal_def)
 
 lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"
   by (simp add: one_ereal_def zero_ereal_def)
@@ -2117,7 +2117,7 @@
   obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
     using * by (force simp: bot_ereal_def)
   then show "bdd_above A" "A \<noteq> {}"
-    by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+    by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp flip: ereal_less_eq)
 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
 
 lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
@@ -2130,7 +2130,7 @@
   obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
     using * by (force simp: top_ereal_def)
   then show "bdd_below A" "A \<noteq> {}"
-    by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+    by (auto intro!: INF_lower bdd_belowI[of _ r] simp flip: ereal_less_eq)
 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
 
 lemma ereal_Inf':
@@ -2527,13 +2527,13 @@
   by (cases n) auto
 
 lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
-  by (cases n) (auto simp: enat_0[symmetric])
+  by (cases n) (auto simp flip: enat_0)
 
 lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
-  by (cases n) (auto simp: enat_0[symmetric])
+  by (cases n) (auto simp flip: enat_0)
 
 lemma ereal_of_enat_zero[simp]: "ereal_of_enat 0 = 0"
-  by (auto simp: enat_0[symmetric])
+  by (auto simp flip: enat_0)
 
 lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
   by (cases n) auto
@@ -3639,7 +3639,7 @@
   by (metis sums_ereal sums_unique summable_def)
 
 lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
-  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
+  by (auto simp: summable_def simp flip: sums_ereal sums_unique)
 
 lemma suminf_ereal_finite_neg:
   assumes "summable f"
@@ -3779,8 +3779,8 @@
     apply auto
     done
   also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
-    using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
-                       simp del: uminus_ereal.simps)
+    using m t by (auto simp: divide_ereal_def mult.commute minus_ereal_def
+                       simp flip: uminus_ereal.simps)
   also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
     using m t
     by (simp add: set_eq_iff image_iff)
@@ -4252,7 +4252,7 @@
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma minus_ereal_0 [simp]: "x - ereal 0 = x"
-by(simp add: zero_ereal_def[symmetric])
+by(simp flip: zero_ereal_def)
 
 lemma ereal_diff_eq_0_iff: fixes a b :: ereal
   shows "(\<bar>a\<bar> = \<infinity> \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity>) \<Longrightarrow> a - b = 0 \<longleftrightarrow> a = b"
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Float.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -82,7 +82,7 @@
     if "e1 \<le> e2" for e1 m1 e2 m2 :: int
   proof -
     from that have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1"
-      by (simp add: powr_realpow[symmetric] powr_diff field_simps)
+      by (simp add: powr_diff field_simps flip: powr_realpow)
     then show ?thesis
       by blast
   qed
@@ -132,7 +132,7 @@
   apply (rename_tac m e)
   apply (rule_tac x="m" in exI)
   apply (rule_tac x="e - d" in exI)
-  apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
+  apply (simp flip: powr_realpow powr_add add: field_simps)
   done
 
 lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
@@ -141,7 +141,7 @@
   apply (rename_tac m e)
   apply (rule_tac x="m" in exI)
   apply (rule_tac x="e - d" in exI)
-  apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
+  apply (simp flip: powr_realpow powr_add add: field_simps)
   done
 
 lemma div_numeral_Bit0_float[simp]:
@@ -549,7 +549,7 @@
     then have "2 powr (exponent f - e) = 2 powr - real_of_int (e - exponent f)"
       by simp
     also have "\<dots> = 1 / 2^nat (e - exponent f)"
-      using pos by (simp add: powr_realpow[symmetric] powr_diff)
+      using pos by (simp flip: powr_realpow add: powr_diff)
     finally have "m * 2^nat (e - exponent f) = real_of_int (mantissa f)"
       using eq by simp
     then have "mantissa f = m * 2^nat (e - exponent f)"
@@ -562,7 +562,7 @@
     then show False using mantissa_not_dvd[OF not_0] by simp
   qed
   ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)"
-    by (simp add: powr_realpow[symmetric])
+    by (simp flip: powr_realpow)
   with \<open>e \<le> exponent f\<close>
   show "m = mantissa f * 2 ^ nat (exponent f - e)"
     by linarith
@@ -662,11 +662,11 @@
 
 lemma round_down_float[simp]: "round_down prec x \<in> float"
   unfolding round_down_def
-  by (auto intro!: times_float simp: of_int_minus[symmetric] simp del: of_int_minus)
+  by (auto intro!: times_float simp flip: of_int_minus)
 
 lemma round_up_float[simp]: "round_up prec x \<in> float"
   unfolding round_up_def
-  by (auto intro!: times_float simp: of_int_minus[symmetric] simp del: of_int_minus)
+  by (auto intro!: times_float simp flip: of_int_minus)
 
 lemma round_up: "x \<le> round_up prec x"
   by (simp add: powr_minus_divide le_divide_eq round_up_def ceiling_correct)
@@ -686,19 +686,19 @@
     by (simp add: round_up_def round_down_def field_simps)
   also have "\<dots> \<le> 1 * 2 powr -prec"
     by (rule mult_mono)
-      (auto simp del: of_int_diff simp: of_int_diff[symmetric] ceiling_diff_floor_le_1)
+      (auto simp flip: of_int_diff simp: ceiling_diff_floor_le_1)
   finally show ?thesis by simp
 qed
 
 lemma round_down_shift: "round_down p (x * 2 powr k) = 2 powr k * round_down (p + k) x"
   unfolding round_down_def
   by (simp add: powr_add powr_mult field_simps powr_diff)
-    (simp add: powr_add[symmetric])
+    (simp flip: powr_add)
 
 lemma round_up_shift: "round_up p (x * 2 powr k) = 2 powr k * round_up (p + k) x"
   unfolding round_up_def
   by (simp add: powr_add powr_mult field_simps powr_diff)
-    (simp add: powr_add[symmetric])
+    (simp flip: powr_add)
 
 lemma round_up_uminus_eq: "round_up p (-x) = - round_down p x"
   and round_down_uminus_eq: "round_down p (-x) = - round_up p x"
@@ -831,7 +831,7 @@
   finally show ?thesis
     using \<open>p + e < 0\<close>
     apply transfer
-    apply (simp add: ac_simps round_down_def floor_divide_of_int_eq[symmetric])
+    apply (simp add: ac_simps round_down_def flip: floor_divide_of_int_eq)
     proof - (*FIXME*)
       fix pa :: int and ea :: int and ma :: int
       assume a1: "2 ^ nat (- pa - ea) = 1 / (2 powr real_of_int pa * 2 powr real_of_int ea)"
@@ -871,8 +871,8 @@
 proof (cases "b dvd a")
   case True
   then show ?thesis
-    by (simp add: ceiling_def of_int_minus[symmetric] divide_minus_left[symmetric]
-      floor_divide_of_int_eq dvd_neg_div del: divide_minus_left of_int_minus)
+    by (simp add: ceiling_def floor_divide_of_int_eq dvd_neg_div
+             flip: of_int_minus divide_minus_left)
 next
   case False
   then have "a mod b \<noteq> 0"
@@ -881,7 +881,7 @@
     using \<open>b \<noteq> 0\<close> by auto
   have "\<lceil>real_of_int a / real_of_int b\<rceil> = \<lfloor>real_of_int a / real_of_int b\<rfloor> + 1"
     apply (rule ceiling_eq)
-    apply (auto simp: floor_divide_of_int_eq[symmetric])
+    apply (auto simp flip: floor_divide_of_int_eq)
   proof -
     have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<le> real_of_int a / real_of_int b"
       by simp
@@ -1207,7 +1207,7 @@
     have "int x * 2 ^ nat l = x'"
       by (simp add: x'_def)
     moreover have "real x * 2 powr l = real x'"
-      by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
+      by (simp flip: powr_realpow add: \<open>0 \<le> l\<close> x'_def)
     ultimately show ?thesis
       using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] \<open>0 \<le> l\<close> \<open>y \<noteq> 0\<close>
         l_def[symmetric, THEN meta_eq_to_obj_eq]
@@ -1223,7 +1223,7 @@
     have "int y * 2 ^ nat (- l) = y'"
       by (simp add: y'_def)
     moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'"
-      using \<open>\<not> 0 \<le> l\<close> by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
+      using \<open>\<not> 0 \<le> l\<close> by (simp flip: powr_realpow add: powr_minus y'_def field_simps)
     ultimately show ?thesis
       using ceil_divide_floor_conv[of y' x] \<open>\<not> 0 \<le> l\<close> \<open>y' \<noteq> 0\<close> \<open>y \<noteq> 0\<close>
         l_def[symmetric, THEN meta_eq_to_obj_eq]
@@ -1389,7 +1389,7 @@
     from that 2 have "(power_down p x (Suc n div 2)) ^ 2 \<le> (x ^ (Suc n div 2)) ^ 2"
       by (auto intro: power_mono power_down_nonneg simp del: odd_Suc_div_two)
     also have "\<dots> = x ^ (Suc n div 2 * 2)"
-      by (simp add: power_mult[symmetric])
+      by (simp flip: power_mult)
     also have "Suc n div 2 * 2 = Suc n"
       using \<open>odd n\<close> by presburger
     finally show ?thesis
@@ -1407,7 +1407,7 @@
     from that even_Suc have "Suc n = Suc n div 2 * 2"
       by presburger
     then have "x ^ Suc n \<le> (x ^ (Suc n div 2))\<^sup>2"
-      by (simp add: power_mult[symmetric])
+      by (simp flip: power_mult)
     also from that 2 have "\<dots> \<le> (power_up p x (Suc n div 2))\<^sup>2"
       by (auto intro: power_mono simp del: odd_Suc_div_two)
     finally show ?thesis
@@ -1506,7 +1506,7 @@
   proof cases
     case 1
     then show ?thesis
-      by (simp add: assms(1)[symmetric] powr_add[symmetric] algebra_simps powr_mult_base)
+      by (simp flip: assms(1) powr_add add: algebra_simps powr_mult_base)
   next
     case 2
     then have "b * 2 powr p < \<bar>b * 2 powr (p + 1)\<bar>"
@@ -1518,12 +1518,12 @@
       by (simp_all add: floor_eq_iff)
 
     have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(a + b) * 2 powr p * 2 powr (q - p)\<rfloor>"
-      by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric])
+      by (simp add: algebra_simps flip: powr_realpow powr_add)
     also have "\<dots> = \<lfloor>(ai + b * 2 powr p) * 2 powr (q - p)\<rfloor>"
       by (simp add: assms algebra_simps)
     also have "\<dots> = \<lfloor>(ai + b * 2 powr p) / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
       using assms
-      by (simp add: algebra_simps powr_realpow[symmetric] divide_powr_uminus powr_add[symmetric])
+      by (simp add: algebra_simps divide_powr_uminus flip: powr_realpow powr_add)
     also have "\<dots> = \<lfloor>ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
       by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
     finally have "\<lfloor>(a + b) * 2 powr real_of_int q\<rfloor> = \<lfloor>real_of_int ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>" .
@@ -1534,7 +1534,7 @@
       have "\<lfloor>(2 * ai + sgn b) * 2 powr (real_of_int (q - p) - 1)\<rfloor> = \<lfloor>(ai + sgn b / 2) * 2 powr (q - p)\<rfloor>"
         by (subst powr_diff) (simp add: field_simps)
       also have "\<dots> = \<lfloor>(ai + sgn b / 2) / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
-        using leqp by (simp add: powr_realpow[symmetric] powr_diff)
+        using leqp by (simp flip: powr_realpow add: powr_diff)
       also have "\<dots> = \<lfloor>ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
         by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
       finally show ?thesis .
@@ -1547,19 +1547,19 @@
       by (auto simp: floor_eq_iff algebra_simps pos_divide_le_eq[symmetric] abs_if divide_powr_uminus
         intro!: mult_neg_pos split: if_split_asm)
     have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2*a + 2*b) * 2 powr p * 2 powr (q - p - 1)\<rfloor>"
-      by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric] powr_mult_base)
+      by (simp add: algebra_simps powr_mult_base flip: powr_realpow powr_add)
     also have "\<dots> = \<lfloor>(2 * (a * 2 powr p) + 2 * b * 2 powr p) * 2 powr (q - p - 1)\<rfloor>"
       by (simp add: algebra_simps)
     also have "\<dots> = \<lfloor>(2 * ai + b * 2 powr (p + 1)) / 2 powr (1 - q + p)\<rfloor>"
       using assms by (simp add: algebra_simps powr_mult_base divide_powr_uminus)
     also have "\<dots> = \<lfloor>(2 * ai + b * 2 powr (p + 1)) / real_of_int ((2::int) ^ nat (p - q + 1))\<rfloor>"
-      using assms by (simp add: algebra_simps powr_realpow[symmetric])
+      using assms by (simp add: algebra_simps flip: powr_realpow)
     also have "\<dots> = \<lfloor>(2 * ai - 1) / real_of_int ((2::int) ^ nat (p - q + 1))\<rfloor>"
       using \<open>b < 0\<close> assms
       by (simp add: floor_divide_of_int_eq floor_eq floor_divide_real_eq_div
         del: of_int_mult of_int_power of_int_diff)
     also have "\<dots> = \<lfloor>(2 * ai - 1) * 2 powr (q - p - 1)\<rfloor>"
-      using assms by (simp add: algebra_simps divide_powr_uminus powr_realpow[symmetric])
+      using assms by (simp add: algebra_simps divide_powr_uminus flip: powr_realpow)
     finally show ?thesis
       using \<open>b < 0\<close> by simp
   qed
@@ -1595,7 +1595,7 @@
       (metis of_int_1 of_int_add of_int_le_numeral_power_cancel_iff)
 
   have "\<bar>ai\<bar> = 2 powr k + r"
-    using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def powr_realpow[symmetric])
+    using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def simp flip: powr_realpow)
 
   have pos: "\<bar>b\<bar> < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
     using \<open>0 \<le> k\<close> \<open>ai \<noteq> 0\<close>
@@ -1664,8 +1664,7 @@
   let ?e = "e1 - int k1 - 1"
 
   have sum_eq: "?sum = (?m1 + ?m2) * 2 powr ?e"
-    by (auto simp: powr_add[symmetric] powr_mult[symmetric] algebra_simps
-      powr_realpow[symmetric] powr_mult_base)
+    by (auto simp flip: powr_add powr_mult powr_realpow simp: powr_mult_base algebra_simps)
 
   have "\<bar>?m2\<bar> * 2 < 2 powr (bitlen \<bar>m2\<bar> + ?shift + 1)"
     by (auto simp: field_simps powr_add powr_mult_base powr_diff abs_mult)
@@ -1753,7 +1752,7 @@
       by (auto simp add: sgn_if zero_less_mult_iff simp del: powr_gt_zero)
     also have "\<lfloor>(real_of_int (2 * ?m1) + real_of_int (sgn m2)) * 2 powr real_of_int (?f - - ?e - 1)\<rfloor> =
         \<lfloor>Float (?m1 * 2 + sgn m2) (?e - 1) * 2 powr ?f\<rfloor>"
-      by (simp add: powr_add[symmetric] algebra_simps powr_realpow[symmetric])
+      by (simp flip: powr_add powr_realpow add: algebra_simps)
     finally
     show "\<lfloor>(?a + ?b) * 2 powr ?f\<rfloor> = \<lfloor>real_of_float (Float (?m1 * 2 + sgn m2) (?e - 1)) * 2 powr ?f\<rfloor>" .
   qed
@@ -1983,7 +1982,7 @@
       have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le>
         x * (2 powr real (Suc prec) / (2 powr log 2 x))"
         using real_of_int_floor_add_one_ge[of "log 2 x"] assms
-        by (auto simp add: algebra_simps powr_diff [symmetric]  intro!: mult_left_mono)
+        by (auto simp: algebra_simps simp flip: powr_diff intro!: mult_left_mono)
       then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> real_of_int ((2::int) ^ (Suc prec))"
         using \<open>0 < x\<close> by (simp add: powr_realpow powr_add)
     qed
@@ -2080,14 +2079,13 @@
       have "x = 2 powr (log 2 \<bar>x\<bar>)" using \<open>0 < x\<close> by simp
       also have "\<dots> \<le> (2 ^ (Suc prec )) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>)"
         using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"] \<open>0 < x\<close>
-        by (auto simp: powr_realpow[symmetric] powr_add[symmetric] algebra_simps
-          powr_mult_base le_powr_iff)
+        by (auto simp flip: powr_realpow powr_add simp: algebra_simps powr_mult_base le_powr_iff)
       also
       have "2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> + 1)"
         using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
         by (auto intro!: floor_mono)
       finally show ?thesis
-        by (auto simp: powr_realpow[symmetric] powr_diff assms of_nat_diff)
+        by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
     qed
     ultimately show ?thesis
       by (metis dual_order.trans truncate_down)
@@ -2170,12 +2168,12 @@
 lemma compute_mantissa[code]:
   "mantissa (Float m e) =
     (if m = 0 then 0 else if 2 dvd m then mantissa (normfloat (Float m e)) else m)"
-  by (auto simp: mantissa_float Float.abs_eq zero_float_def[symmetric])
+  by (auto simp: mantissa_float Float.abs_eq simp flip: zero_float_def)
 
 lemma compute_exponent[code]:
   "exponent (Float m e) =
     (if m = 0 then 0 else if 2 dvd m then exponent (normfloat (Float m e)) else e)"
-  by (auto simp: exponent_float Float.abs_eq zero_float_def[symmetric])
+  by (auto simp: exponent_float Float.abs_eq simp flip: zero_float_def)
 
 lifting_update Float.float.lifting
 lifting_forget Float.float.lifting
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Going_To_Filter.thy
--- a/src/HOL/Library/Going_To_Filter.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Going_To_Filter.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -80,7 +80,7 @@
 
 lemma going_to_within_union [simp]: 
   "f going_to F within (A \<union> B) = sup (f going_to F within A) (f going_to F within B)"
-  by (simp add: going_to_within_def inf_sup_distrib1 [symmetric])
+  by (simp add: going_to_within_def flip: inf_sup_distrib1)
 
 lemma eventually_going_to_at_top_linorder:
   fixes f :: "'a \<Rightarrow> 'b :: linorder"
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
 
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -1524,7 +1524,7 @@
   proof (cases p q rule: linorder_cases)
     assume "p < q"
     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
-      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
     with `p < q` show ?thesis by auto
   next
     assume "p = q"
@@ -1533,7 +1533,7 @@
   next
     assume "p > q"
     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
-      by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp: powr_diff [symmetric] )
+      by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
     with B `p > q` show ?thesis by auto
   qed
 qed
@@ -1555,7 +1555,7 @@
   proof (cases p q rule: linorder_cases)
     assume "p < q"
     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
-      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
     with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
   next
     assume "p = q"
@@ -1564,7 +1564,7 @@
   next
     assume "p > q"
     hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
-      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
     with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
   qed
 qed
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -136,7 +136,7 @@
 qed
 
 lemma prts: "a = pprt a + nprt a"
-  by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
+  by (simp add: pprt_def nprt_def flip: add_eq_inf_sup)
 
 lemma zero_le_pprt[simp]: "0 \<le> pprt a"
   by (simp add: pprt_def)
@@ -266,7 +266,7 @@
 proof -
   from add_le_cancel_left [of "uminus a" "plus a a" zero]
   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
-    by (simp add: add.assoc[symmetric])
+    by (simp flip: add.assoc)
   then show ?thesis
     by simp
 qed
@@ -275,7 +275,7 @@
 proof -
   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
     using add_le_cancel_left [of "uminus a" zero "plus a a"]
-    by (simp add: add.assoc[symmetric])
+    by (simp flip: add.assoc)
   then show ?thesis
     by simp
 qed
@@ -461,7 +461,7 @@
       apply blast
       done
     have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
-      by (simp add: prts[symmetric])
+      by (simp flip: prts)
     show ?thesis
     proof (cases "0 \<le> a * b")
       case True
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -531,7 +531,7 @@
        (auto simp: stl)
 next
   assume "alw (\<lambda>x. P (f x)) s" then show "alw P (f s)"
-    by (coinduction arbitrary: s rule: alw_coinduct) (auto simp: stl[symmetric])
+    by (coinduction arbitrary: s rule: alw_coinduct) (auto simp flip: stl)
 qed
 
 lemma ev_inv:
@@ -542,7 +542,7 @@
     by (induction "f s" arbitrary: s) (auto simp: stl)
 next
   assume "ev (\<lambda>x. P (f x)) s" then show "ev P (f s)"
-    by induction (auto simp: stl[symmetric])
+    by induction (auto simp flip: stl)
 qed
 
 lemma alw_smap: "alw P (smap f s) \<longleftrightarrow> alw (\<lambda>x. P (smap f x)) s"
@@ -624,7 +624,7 @@
     by (induction "f s" arbitrary: s) (auto simp: stl intro: suntil.intros)
 next
   assume "((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s" then show "(P suntil Q) (f s)"
-    by induction (auto simp: stl[symmetric] intro: suntil.intros)
+    by induction (auto simp flip: stl intro: suntil.intros)
 qed
 
 lemma suntil_smap: "(P suntil Q) (smap f s) \<longleftrightarrow> ((\<lambda>x. P (smap f x)) suntil (\<lambda>x. Q (smap f x))) s"
@@ -778,7 +778,7 @@
     using \<open>alw (HLD s) \<omega>\<close> by (simp add: alw_iff_sdrop HLD_iff)
   from pigeonhole_infinite_rel[OF infinite_UNIV_nat \<open>finite s\<close> this]
   show ?thesis
-    by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
+    by (simp add: HLD_iff flip: infinite_iff_alw_ev)
 qed
 
 lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>"
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Log_Nat.thy
--- a/src/HOL/Library/Log_Nat.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Log_Nat.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -37,7 +37,7 @@
     also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)"
       using assms by (intro powr_less_mono) auto
     also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)"
-      using assms by (simp add: powr_realpow[symmetric])
+      using assms by (simp flip: powr_realpow)
     finally
     have "x < b ^ nat (\<lfloor>log b (int x)\<rfloor> + 1)"
       by (rule of_nat_less_imp_less)
@@ -182,7 +182,7 @@
       by (auto simp: )
     then have "?l \<le> b powr log (real b) (real x)"
       using \<open>b > 1\<close>
-      by (auto simp add: powr_realpow[symmetric] intro!: powr_mono of_nat_floor)
+      by (auto simp flip: powr_realpow intro!: powr_mono of_nat_floor)
     also have "\<dots> = x" using \<open>b > 1\<close> \<open>0 < x\<close>
       by auto
     finally show ?thesis
@@ -269,7 +269,7 @@
 
 lemma bitlen_ge_iff_power: "w \<le> bitlen x \<longleftrightarrow> w \<le> 0 \<or> 2 ^ (nat w - 1) \<le> x"
   unfolding bitlen_def
-  by (auto simp: nat_le_iff[symmetric] intro: floorlog_geI dest: floorlog_geD)
+  by (auto simp flip: nat_le_iff intro: floorlog_geI dest: floorlog_geD)
 
 lemma bitlen_twopow_add_eq: "bitlen (2 ^ w + b) = w + 1" if "0 \<le> b" "b < 2 ^ w"
   by (auto simp: that nat_add_distrib bitlen_le_iff_power bitlen_ge_iff_power intro!: antisym)
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -101,7 +101,7 @@
 lemma add_mset_in_multiset:
   assumes M: \<open>M \<in> multiset\<close>
   shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
-  using assms by (simp add: multiset_def insert_Collect[symmetric])
+  using assms by (simp add: multiset_def flip: insert_Collect)
 
 lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
   "\<lambda>a M b. if b = a then Suc (M b) else M b"
@@ -244,8 +244,7 @@
   using count [of M] by (simp add: multiset_def)
 
 lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
-  by (auto simp del: count_greater_eq_Suc_zero_iff
-      simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)
+  by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits)
 
 lemma multiset_nonemptyE [elim]:
   assumes "A \<noteq> {#}"
@@ -1216,8 +1215,8 @@
       using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
     hence "Sup A \<subseteq># Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
     with \<open>x \<in># Sup A\<close> show False
-      by (auto simp: subseteq_mset_def count_greater_zero_iff [symmetric]
-               simp del: count_greater_zero_iff dest!: spec[of _ x])
+      by (auto simp: subseteq_mset_def simp flip: count_greater_zero_iff
+               dest!: spec[of _ x])
   qed
 next
   fix x X assume "x \<in> set_mset X" "X \<in> A"
@@ -2158,7 +2157,7 @@
 lemma replicate_mset_msubseteq_iff:
   "replicate_mset m a \<subseteq># replicate_mset n b \<longleftrightarrow> m = 0 \<or> a = b \<and> m \<le> n"
   by (cases m)
-    (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
+    (auto simp: insert_subset_eq_iff simp flip: count_le_replicate_mset_subset_eq)
 
 lemma msubseteq_replicate_msetE:
   assumes "A \<subseteq># replicate_mset n a"
@@ -2991,7 +2990,7 @@
   assumes "trans s" and "irrefl s"
   shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
 proof -
-  have "X - X \<inter># Y + X \<inter># Y = X" "Y - X \<inter># Y + X \<inter># Y = Y" by (auto simp: count_inject[symmetric])
+  have "X - X \<inter># Y + X \<inter># Y = X" "Y - X \<inter># Y + X \<inter># Y = Y" by (auto simp flip: count_inject)
   thus ?thesis using mult_cancel[OF assms, of "X - X \<inter># Y"  "X \<inter># Y" "Y - X \<inter># Y"] by auto
 qed
 
@@ -3020,7 +3019,7 @@
   shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
 proof -
   have *: "M \<inter># N + (N - M \<inter># N) = N" "M \<inter># N + (M - M \<inter># N) = M"
-    "(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp: count_inject[symmetric])
+    "(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp flip: count_inject)
   show ?thesis
   proof
     assume ?L thus ?R
@@ -3041,9 +3040,9 @@
   shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
 proof -
   { assume "N \<noteq> M" "M - M \<inter># N = {#}"
-    then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric])
+    then obtain y where "count N y \<noteq> count M y" by (auto simp flip: count_inject)
     then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
-      by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y])
+      by (auto simp flip: count_inject dest!: le_neq_implies_less fun_cong[of _ _ y])
   }
   then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
     by (auto simp: multeqp_def multp_def Let_def in_diff_count)
@@ -3695,7 +3694,7 @@
     apply (rule ext)+
     apply safe
      apply (rule_tac x = "mset (zip xs ys)" in exI;
-       auto simp: in_set_zip list_all2_iff mset_map[symmetric])
+       auto simp: in_set_zip list_all2_iff simp flip: mset_map)
     apply (rename_tac XY)
     apply (cut_tac X = XY in ex_mset)
     apply (erule exE)
@@ -3894,7 +3893,7 @@
   using arg_cong[OF insert_DiffM, of _ _ size] by simp
 
 lemma size_Diff_singleton: "x \<in># M \<Longrightarrow> size (M - {#x#}) = size M - 1"
-  by (simp add: size_Suc_Diff1 [symmetric])
+  by (simp flip: size_Suc_Diff1)
 
 lemma size_Diff_singleton_if: "size (A - {#x#}) = (if x \<in># A then size A - 1 else size A)"
   by (simp add: diff_single_trivial size_Diff_singleton)
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Multiset_Permutations.thy
--- a/src/HOL/Library/Multiset_Permutations.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Multiset_Permutations.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -216,7 +216,7 @@
 theorem card_permutations_of_multiset:
   "card (permutations_of_multiset A) = fact (size A) div (\<Prod>x\<in>set_mset A. fact (count A x))"
   "(\<Prod>x\<in>set_mset A. fact (count A x) :: nat) dvd fact (size A)"
-  by (simp_all add: card_permutations_of_multiset_aux[of A, symmetric])
+  by (simp_all flip: card_permutations_of_multiset_aux[of A])
 
 lemma card_permutations_of_multiset_insert_aux:
   "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) = 
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Periodic_Fun.thy
--- a/src/HOL/Library/Periodic_Fun.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Periodic_Fun.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -54,7 +54,7 @@
   by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)
 
 lemma minus_1: "f (gn1 x) = f x"
-  using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric])
+  using minus_of_nat[of x 1] by (simp flip: minus_1_eq minus_eq)
 
 lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int 
                         plus_numeral minus_numeral plus_1 minus_1
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Perm.thy
--- a/src/HOL/Library/Perm.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Perm.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -79,7 +79,7 @@
   then obtain a where *: "affected f = {a}"
     by (rule card_1_singletonE)
   then have **: "f \<langle>$\<rangle> a \<noteq> a"
-    by (simp add: in_affected [symmetric])
+    by (simp flip: in_affected)
   with * have "f \<langle>$\<rangle> a \<notin> affected f"
     by simp
   then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
@@ -545,7 +545,7 @@
   have "(f ^ n) \<langle>$\<rangle> a = (f ^ (n mod order f a + order f a * (n div order f a))) \<langle>$\<rangle> a"
     by simp
   also have "\<dots> = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) \<langle>$\<rangle> a"
-    by (simp add: power_add [symmetric])
+    by (simp flip: power_add)
   finally show ?thesis
     by (simp add: apply_times)
 qed  
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Stirling.thy
--- a/src/HOL/Library/Stirling.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Stirling.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -195,7 +195,7 @@
     by (subst sum_atMost_Suc_shift) (simp add: sum.distrib ring_distribs)
   also have "\<dots> = pochhammer x (Suc n)"
     by (subst sum_atMost_Suc_shift [symmetric])
-      (simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc Suc [symmetric])
+      (simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc flip: Suc)
   finally show ?case .
 qed
 
@@ -262,7 +262,7 @@
   also have "zip_with_prev f y ys = map (\<lambda>i. f (xs ! i) (xs ! (i + 1))) [0..<length xs - 1]"
     unfolding Cons
     by (induct ys arbitrary: y)
-      (simp_all add: zip_with_prev_def upt_conv_Cons map_Suc_upt [symmetric] del: upt_Suc)
+      (simp_all add: zip_with_prev_def upt_conv_Cons flip: map_Suc_upt del: upt_Suc)
   finally show ?thesis
     using Cons by simp
 qed
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Stream.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -430,8 +430,8 @@
 
 lemma stream_smap_fromN: "s = smap (\<lambda>j. let i = j - n in s !! i) (fromN n)"
   by (coinduction arbitrary: s n)
-    (force simp: neq_Nil_conv Let_def snth.simps(2)[symmetric] Suc_diff_Suc
-      intro: stream.map_cong split: if_splits simp del: snth.simps(2))
+    (force simp: neq_Nil_conv Let_def Suc_diff_Suc simp flip: snth.simps(2)
+      intro: stream.map_cong split: if_splits)
 
 lemma stream_smap_nats: "s = smap (snth s) nats"
   using stream_smap_fromN[where n = 0] by simp
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Sublist.thy
--- 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
 
diff -r 6a0852b8e5a8 -r 6beb45f6cf67 src/HOL/Library/Uprod.thy
--- a/src/HOL/Library/Uprod.thy	Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Uprod.thy	Thu Jun 07 19:36:12 2018 +0200
@@ -129,7 +129,7 @@
   show "card_order natLeq" by(rule natLeq_card_order)
   show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by(rule natLeq_cinfinite)
   show "ordLeq3 (card_of (set_uprod x)) natLeq" for x :: "'a uprod"
-    by (auto simp: finite_iff_ordLess_natLeq[symmetric] intro: ordLess_imp_ordLeq)
+    by (auto simp flip: finite_iff_ordLess_natLeq intro: ordLess_imp_ordLeq)
   show "rel_uprod R OO rel_uprod S \<le> rel_uprod (R OO S)"
     for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" by(rule predicate2I)(transfer; auto)
   show "rel_uprod R = (\<lambda>x y. \<exists>z. set_uprod z \<subseteq> {(x, y). R x y} \<and> map_uprod fst z = x \<and> map_uprod snd z = y)"