src/HOL/Int.thy
changeset 61552 980dd46a03fb
parent 61531 ab2e862263e7
child 61609 77b453bd616f
     1.1 --- a/src/HOL/Int.thy	Mon Nov 02 11:56:38 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Mon Nov 02 16:17:09 2015 +0100
     1.3 @@ -686,6 +686,9 @@
     1.4  lemma Ints_1 [simp]: "1 \<in> \<int>"
     1.5    using Ints_of_int [of "1"] by simp
     1.6  
     1.7 +lemma Ints_numeral [simp]: "numeral n \<in> \<int>"
     1.8 +  by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
     1.9 +
    1.10  lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
    1.11  apply (auto simp add: Ints_def)
    1.12  apply (rule range_eqI)