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.9
1.10  lemma zero_le_pprt[simp]: "0 \<le> pprt a"
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.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.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
```