src/HOL/OrderedGroup.thy
changeset 29833 409138c4de12
parent 29670 cbe35f4f04f8
child 29886 b8a6b9c56fdd
     1.1 --- a/src/HOL/OrderedGroup.thy	Sat Feb 07 10:56:44 2009 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Sun Feb 08 11:59:26 2009 +0100
     1.3 @@ -598,12 +598,12 @@
     1.4  by (simp add: algebra_simps)
     1.5  
     1.6  text{*Legacy - use @{text algebra_simps} *}
     1.7 -lemmas group_simps = algebra_simps
     1.8 +lemmas group_simps[noatp] = algebra_simps
     1.9  
    1.10  end
    1.11  
    1.12  text{*Legacy - use @{text algebra_simps} *}
    1.13 -lemmas group_simps = algebra_simps
    1.14 +lemmas group_simps[noatp] = algebra_simps
    1.15  
    1.16  class ordered_ab_semigroup_add =
    1.17    linorder + pordered_ab_semigroup_add
    1.18 @@ -1310,9 +1310,9 @@
    1.19    add_less_le_mono add_le_less_mono add_strict_mono)
    1.20  
    1.21  text{*Simplification of @{term "x-y < 0"}, etc.*}
    1.22 -lemmas diff_less_0_iff_less [simp] = less_iff_diff_less_0 [symmetric]
    1.23 +lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
    1.24  lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
    1.25 -lemmas diff_le_0_iff_le [simp] = le_iff_diff_le_0 [symmetric]
    1.26 +lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
    1.27  
    1.28  ML {*
    1.29  structure ab_group_add_cancel = Abel_Cancel