src/HOL/Library/Lattice_Algebras.thy
changeset 68406 6beb45f6cf67
parent 65151 a7394aa4d21c
     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Thu Jun 07 15:08:18 2018 +0200
     1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Jun 07 19:36:12 2018 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  qed
     1.5  
     1.6  lemma prts: "a = pprt a + nprt a"
     1.7 -  by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
     1.8 +  by (simp add: pprt_def nprt_def flip: add_eq_inf_sup)
     1.9  
    1.10  lemma zero_le_pprt[simp]: "0 \<le> pprt a"
    1.11    by (simp add: pprt_def)
    1.12 @@ -266,7 +266,7 @@
    1.13  proof -
    1.14    from add_le_cancel_left [of "uminus a" "plus a a" zero]
    1.15    have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
    1.16 -    by (simp add: add.assoc[symmetric])
    1.17 +    by (simp flip: add.assoc)
    1.18    then show ?thesis
    1.19      by simp
    1.20  qed
    1.21 @@ -275,7 +275,7 @@
    1.22  proof -
    1.23    have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
    1.24      using add_le_cancel_left [of "uminus a" zero "plus a a"]
    1.25 -    by (simp add: add.assoc[symmetric])
    1.26 +    by (simp flip: add.assoc)
    1.27    then show ?thesis
    1.28      by simp
    1.29  qed
    1.30 @@ -461,7 +461,7 @@
    1.31        apply blast
    1.32        done
    1.33      have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
    1.34 -      by (simp add: prts[symmetric])
    1.35 +      by (simp flip: prts)
    1.36      show ?thesis
    1.37      proof (cases "0 \<le> a * b")
    1.38        case True