diff -r 10e723e54076 -r c5f54c04a1aa src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Int.thy	Thu Mar 18 13:14:54 2010 +0100
@@ -86,7 +86,7 @@
 
 text{*Reduces equality on abstractions to equality on representatives:
   @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
-declare Abs_Integ_inject [simp,noatp]  Abs_Integ_inverse [simp,noatp]
+declare Abs_Integ_inject [simp,no_atp]  Abs_Integ_inverse [simp,no_atp]
 
 text{*Case analysis on the representation of an integer as an equivalence
       class of pairs of naturals.*}
@@ -522,7 +522,7 @@
       It is proved here because attribute @{text arith_split} is not available
       in theory @{text Rings}.
       But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split [arith_split,noatp]:
+lemma abs_split [arith_split,no_atp]:
      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
@@ -1875,16 +1875,16 @@
 
 text{*These are actually for fields, like real: but where else to put them?*}
 
-lemmas zero_less_divide_iff_number_of [simp, noatp] =
+lemmas zero_less_divide_iff_number_of [simp, no_atp] =
   zero_less_divide_iff [of "number_of w", standard]
 
-lemmas divide_less_0_iff_number_of [simp, noatp] =
+lemmas divide_less_0_iff_number_of [simp, no_atp] =
   divide_less_0_iff [of "number_of w", standard]
 
-lemmas zero_le_divide_iff_number_of [simp, noatp] =
+lemmas zero_le_divide_iff_number_of [simp, no_atp] =
   zero_le_divide_iff [of "number_of w", standard]
 
-lemmas divide_le_0_iff_number_of [simp, noatp] =
+lemmas divide_le_0_iff_number_of [simp, no_atp] =
   divide_le_0_iff [of "number_of w", standard]
 
 
@@ -1897,53 +1897,53 @@
 text {*These laws simplify inequalities, moving unary minus from a term
 into the literal.*}
 
-lemmas less_minus_iff_number_of [simp, noatp] =
+lemmas less_minus_iff_number_of [simp, no_atp] =
   less_minus_iff [of "number_of v", standard]
 
-lemmas le_minus_iff_number_of [simp, noatp] =
+lemmas le_minus_iff_number_of [simp, no_atp] =
   le_minus_iff [of "number_of v", standard]
 
-lemmas equation_minus_iff_number_of [simp, noatp] =
+lemmas equation_minus_iff_number_of [simp, no_atp] =
   equation_minus_iff [of "number_of v", standard]
 
-lemmas minus_less_iff_number_of [simp, noatp] =
+lemmas minus_less_iff_number_of [simp, no_atp] =
   minus_less_iff [of _ "number_of v", standard]
 
-lemmas minus_le_iff_number_of [simp, noatp] =
+lemmas minus_le_iff_number_of [simp, no_atp] =
   minus_le_iff [of _ "number_of v", standard]
 
-lemmas minus_equation_iff_number_of [simp, noatp] =
+lemmas minus_equation_iff_number_of [simp, no_atp] =
   minus_equation_iff [of _ "number_of v", standard]
 
 
 text{*To Simplify Inequalities Where One Side is the Constant 1*}
 
-lemma less_minus_iff_1 [simp,noatp]:
+lemma less_minus_iff_1 [simp,no_atp]:
   fixes b::"'b::{linordered_idom,number_ring}"
   shows "(1 < - b) = (b < -1)"
 by auto
 
-lemma le_minus_iff_1 [simp,noatp]:
+lemma le_minus_iff_1 [simp,no_atp]:
   fixes b::"'b::{linordered_idom,number_ring}"
   shows "(1 \<le> - b) = (b \<le> -1)"
 by auto
 
-lemma equation_minus_iff_1 [simp,noatp]:
+lemma equation_minus_iff_1 [simp,no_atp]:
   fixes b::"'b::number_ring"
   shows "(1 = - b) = (b = -1)"
 by (subst equation_minus_iff, auto)
 
-lemma minus_less_iff_1 [simp,noatp]:
+lemma minus_less_iff_1 [simp,no_atp]:
   fixes a::"'b::{linordered_idom,number_ring}"
   shows "(- a < 1) = (-1 < a)"
 by auto
 
-lemma minus_le_iff_1 [simp,noatp]:
+lemma minus_le_iff_1 [simp,no_atp]:
   fixes a::"'b::{linordered_idom,number_ring}"
   shows "(- a \<le> 1) = (-1 \<le> a)"
 by auto
 
-lemma minus_equation_iff_1 [simp,noatp]:
+lemma minus_equation_iff_1 [simp,no_atp]:
   fixes a::"'b::number_ring"
   shows "(- a = 1) = (a = -1)"
 by (subst minus_equation_iff, auto)
@@ -1951,16 +1951,16 @@
 
 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
 
-lemmas mult_less_cancel_left_number_of [simp, noatp] =
+lemmas mult_less_cancel_left_number_of [simp, no_atp] =
   mult_less_cancel_left [of "number_of v", standard]
 
-lemmas mult_less_cancel_right_number_of [simp, noatp] =
+lemmas mult_less_cancel_right_number_of [simp, no_atp] =
   mult_less_cancel_right [of _ "number_of v", standard]
 
-lemmas mult_le_cancel_left_number_of [simp, noatp] =
+lemmas mult_le_cancel_left_number_of [simp, no_atp] =
   mult_le_cancel_left [of "number_of v", standard]
 
-lemmas mult_le_cancel_right_number_of [simp, noatp] =
+lemmas mult_le_cancel_right_number_of [simp, no_atp] =
   mult_le_cancel_right [of _ "number_of v", standard]