src/HOL/Library/Lattice_Algebras.thy
changeset 57862 8f074e6e22fc
parent 57512 cc97b347b301
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Tue Aug 05 12:42:38 2014 +0200
     1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Tue Aug 05 12:56:15 2014 +0200
     1.3 @@ -396,7 +396,7 @@
     1.4    proof -
     1.5      have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
     1.6        (is "_=sup ?m ?n")
     1.7 -      by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
     1.8 +      by (simp add: abs_lattice add_sup_inf_distribs ac_simps)
     1.9      have a: "a + b \<le> sup ?m ?n"
    1.10        by simp
    1.11      have b: "- a - b \<le> ?n"
    1.12 @@ -410,7 +410,7 @@
    1.13      from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
    1.14        apply -
    1.15        apply (drule abs_leI)
    1.16 -      apply (simp_all only: algebra_simps ac_simps minus_add)
    1.17 +      apply (simp_all only: algebra_simps minus_add)
    1.18        apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
    1.19        done
    1.20      with g[symmetric] show ?thesis by simp