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.14    by (simp add: less_Suc_eq)
    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"