src/HOL/Groups.thy
changeset 54148 c8cc5ab4a863
parent 54147 97a8ff4e4ac9
child 54230 b1d955791529
     1.1 --- a/src/HOL/Groups.thy	Fri Oct 18 10:43:20 2013 +0200
     1.2 +++ b/src/HOL/Groups.thy	Fri Oct 18 10:43:21 2013 +0200
     1.3 @@ -517,7 +517,7 @@
     1.4  
     1.5  (* FIXME: duplicates right_minus_eq from class group_add *)
     1.6  (* but only this one is declared as a simp rule. *)
     1.7 -lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
     1.8 +lemma diff_eq_0_iff_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
     1.9    by (rule right_minus_eq)
    1.10  
    1.11  lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
    1.12 @@ -896,7 +896,7 @@
    1.13  lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
    1.14  by (auto simp add: le_less minus_less_iff)
    1.15  
    1.16 -lemma diff_less_0_iff_less [simp, no_atp]:
    1.17 +lemma diff_less_0_iff_less [simp]:
    1.18    "a - b < 0 \<longleftrightarrow> a < b"
    1.19  proof -
    1.20    have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
    1.21 @@ -924,7 +924,7 @@
    1.22  lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
    1.23  by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
    1.24  
    1.25 -lemma diff_le_0_iff_le [simp, no_atp]:
    1.26 +lemma diff_le_0_iff_le [simp]:
    1.27    "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
    1.28    by (simp add: algebra_simps)
    1.29  
    1.30 @@ -1231,7 +1231,7 @@
    1.31  lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
    1.32  by simp
    1.33  
    1.34 -lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
    1.35 +lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
    1.36  proof -
    1.37    have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
    1.38    thus ?thesis by simp