src/HOL/Library/Lattice_Algebras.thy
 changeset 57512 cc97b347b301 parent 56228 0f6dc7512023 child 57862 8f074e6e22fc
```     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Fri Jul 04 20:07:08 2014 +0200
1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Fri Jul 04 20:18:47 2014 +0200
1.3 @@ -13,7 +13,7 @@
1.4    apply (rule antisym)
1.6    apply (rule add_le_imp_le_left [of "uminus a"])
1.9    done
1.10
1.11  lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
1.12 @@ -21,7 +21,7 @@
1.13    have "c + inf a b = inf (c + a) (c + b)"
1.15    then show ?thesis
1.18  qed
1.19
1.20  end
1.21 @@ -32,10 +32,10 @@
1.22  lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
1.23    apply (rule antisym)
1.24    apply (rule add_le_imp_le_left [of "uminus a"])
1.25 -  apply (simp only: add_assoc [symmetric], simp)
1.26 +  apply (simp only: add.assoc [symmetric], simp)
1.28    apply (rule le_supI)
1.31    done
1.32
1.33  lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
1.34 @@ -43,7 +43,7 @@
1.35    have "c + sup a b = sup (c+a) (c+b)"
1.37    then show ?thesis
1.40  qed
1.41
1.42  end
1.43 @@ -151,7 +151,7 @@
1.44    then show ?r
1.45      apply -
1.46      apply (rule add_le_imp_le_right[of _ "uminus b" _])
1.49      done
1.50  next
1.51    assume ?r
1.52 @@ -243,7 +243,7 @@
1.53    then have "a + a + - a = - a"
1.54      by simp
1.55    then have "a + (a + - a) = - a"
1.56 -    by (simp only: add_assoc)
1.57 +    by (simp only: add.assoc)
1.58    then have a: "- a = a"
1.59      by simp
1.60    show "a = 0"
1.61 @@ -309,7 +309,7 @@
1.62  proof -
1.63    from add_le_cancel_left [of "uminus a" "plus a a" zero]
1.64    have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"