src/HOL/Nat.thy
changeset 54147 97a8ff4e4ac9
parent 53986 a269577d97c0
child 54222 24874b4024d1
     1.1 --- a/src/HOL/Nat.thy	Fri Oct 18 10:35:57 2013 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Oct 18 10:43:20 2013 +0200
     1.3 @@ -327,7 +327,7 @@
     1.4     apply auto
     1.5    done
     1.6  
     1.7 -lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
     1.8 +lemma one_eq_mult_iff [simp]: "(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, fastforce)
    1.11    done
    1.12 @@ -491,7 +491,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, no_atp]: "(n < (1::nat)) = (n = 0)"
    1.17 +lemma less_one [iff]: "(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 @@ -659,7 +659,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,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
    1.26 +lemma not_gr0 [iff]: "!!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 @@ -1396,10 +1396,10 @@
    1.31  
    1.32  text{*Special cases where either operand is zero*}
    1.33  
    1.34 -lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
    1.35 +lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
    1.36    by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
    1.37  
    1.38 -lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
    1.39 +lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
    1.40    by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
    1.41  
    1.42  end
    1.43 @@ -1432,7 +1432,7 @@
    1.44  
    1.45  text{*Special cases where either operand is zero*}
    1.46  
    1.47 -lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
    1.48 +lemma of_nat_le_0_iff [simp]: "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"