--- a/src/HOL/Nat.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Nat.thy Thu Mar 18 12:58:52 2010 +0100
@@ -320,7 +320,7 @@
apply auto
done
-lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
+lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
apply (rule trans)
apply (rule_tac [2] mult_eq_1_iff, fastsimp)
done
@@ -480,7 +480,7 @@
lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
by (simp add: less_Suc_eq)
-lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+lemma less_one [iff, no_atp]: "(n < (1::nat)) = (n = 0)"
unfolding One_nat_def by (rule less_Suc0)
lemma Suc_mono: "m < n ==> Suc m < Suc n"
@@ -648,7 +648,7 @@
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
by (fast intro: not0_implies_Suc)
-lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
+lemma not_gr0 [iff,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
using neq0_conv by blast
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
@@ -1279,10 +1279,10 @@
text{*Special cases where either operand is zero*}
-lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
+lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
-lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
+lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
lemma inj_of_nat: "inj of_nat"
@@ -1327,7 +1327,7 @@
lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
by (rule of_nat_le_iff [of 0, simplified])
-lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
+lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
by (rule of_nat_le_iff [of _ 0, simplified])
lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"