src/HOL/Nat.thy
 changeset 35828 46cfc4b8112e parent 35633 5da59c1ddece child 36176 3fe7e97ccca8
```     1.1 --- a/src/HOL/Nat.thy	Wed Mar 17 19:37:44 2010 +0100
1.2 +++ b/src/HOL/Nat.thy	Thu Mar 18 12:58:52 2010 +0100
1.3 @@ -320,7 +320,7 @@
1.4     apply auto
1.5    done
1.6
1.7 -lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
1.8 +lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
1.9    apply (rule trans)
1.10    apply (rule_tac [2] mult_eq_1_iff, fastsimp)
1.11    done
1.12 @@ -480,7 +480,7 @@
1.13  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
1.15
1.16 -lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
1.17 +lemma less_one [iff, no_atp]: "(n < (1::nat)) = (n = 0)"
1.18    unfolding One_nat_def by (rule less_Suc0)
1.19
1.20  lemma Suc_mono: "m < n ==> Suc m < Suc n"
1.21 @@ -648,7 +648,7 @@
1.22  lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
1.23  by (fast intro: not0_implies_Suc)
1.24
1.25 -lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
1.26 +lemma not_gr0 [iff,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
1.27  using neq0_conv by blast
1.28
1.29  lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
1.30 @@ -1279,10 +1279,10 @@
1.31
1.32  text{*Special cases where either operand is zero*}
1.33
1.34 -lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
1.35 +lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
1.36    by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
1.37
1.38 -lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
1.39 +lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
1.40    by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
1.41
1.42  lemma inj_of_nat: "inj of_nat"
1.43 @@ -1327,7 +1327,7 @@
1.44  lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
1.45    by (rule of_nat_le_iff [of 0, simplified])
1.46
1.47 -lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
1.48 +lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
1.49    by (rule of_nat_le_iff [of _ 0, simplified])
1.50
1.51  lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
```