src/HOL/Rings.thy
changeset 54147 97a8ff4e4ac9
parent 52435 6646bb548c6b
child 54225 8a49a5a30284
     1.1 --- a/src/HOL/Rings.thy	Fri Oct 18 10:35:57 2013 +0200
     1.2 +++ b/src/HOL/Rings.thy	Fri Oct 18 10:43:20 2013 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    then show ?thesis ..
     1.5  qed
     1.6  
     1.7 -lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
     1.8 +lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
     1.9  by (auto intro: dvd_refl elim!: dvdE)
    1.10  
    1.11  lemma dvd_0_right [iff]: "a dvd 0"
    1.12 @@ -233,8 +233,8 @@
    1.13  by (rule minus_unique) (simp add: distrib_left [symmetric]) 
    1.14  
    1.15  text{*Extract signs from products*}
    1.16 -lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
    1.17 -lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
    1.18 +lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
    1.19 +lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
    1.20  
    1.21  lemma minus_mult_minus [simp]: "- a * - b = a * b"
    1.22  by simp
    1.23 @@ -248,7 +248,7 @@
    1.24  lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
    1.25  by (simp add: distrib_right diff_minus)
    1.26  
    1.27 -lemmas ring_distribs[no_atp] =
    1.28 +lemmas ring_distribs =
    1.29    distrib_left distrib_right left_diff_distrib right_diff_distrib
    1.30  
    1.31  lemma eq_add_iff1:
    1.32 @@ -261,7 +261,7 @@
    1.33  
    1.34  end
    1.35  
    1.36 -lemmas ring_distribs[no_atp] =
    1.37 +lemmas ring_distribs =
    1.38    distrib_left distrib_right left_diff_distrib right_diff_distrib
    1.39  
    1.40  class comm_ring = comm_semiring + ab_group_add
    1.41 @@ -336,7 +336,7 @@
    1.42  qed
    1.43  
    1.44  text{*Cancellation of equalities with a common factor*}
    1.45 -lemma mult_cancel_right [simp, no_atp]:
    1.46 +lemma mult_cancel_right [simp]:
    1.47    "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
    1.48  proof -
    1.49    have "(a * c = b * c) = ((a - b) * c = 0)"
    1.50 @@ -344,7 +344,7 @@
    1.51    thus ?thesis by (simp add: disj_commute)
    1.52  qed
    1.53  
    1.54 -lemma mult_cancel_left [simp, no_atp]:
    1.55 +lemma mult_cancel_left [simp]:
    1.56    "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
    1.57  proof -
    1.58    have "(c * a = c * b) = (c * (a - b) = 0)"
    1.59 @@ -1048,7 +1048,7 @@
    1.60  
    1.61  text {* Simprules for comparisons where common factors can be cancelled. *}
    1.62  
    1.63 -lemmas mult_compare_simps[no_atp] =
    1.64 +lemmas mult_compare_simps =
    1.65      mult_le_cancel_right mult_le_cancel_left
    1.66      mult_le_cancel_right1 mult_le_cancel_right2
    1.67      mult_le_cancel_left1 mult_le_cancel_left2