src/HOL/Real.thy
changeset 61070 b72a990adfe2
parent 60758 d8d85a8172b5
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Real.thy	Mon Aug 31 21:01:21 2015 +0200
     1.2 +++ b/src/HOL/Real.thy	Mon Aug 31 21:28:08 2015 +0200
     1.3 @@ -1163,7 +1163,7 @@
     1.4  lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
     1.5  by (insert real_of_int_div2 [of n x], simp)
     1.6  
     1.7 -lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
     1.8 +lemma Ints_real_of_int [simp]: "real (x::int) \<in> \<int>"
     1.9  unfolding real_of_int_def by (rule Ints_of_int)
    1.10  
    1.11  
    1.12 @@ -1300,10 +1300,10 @@
    1.13    apply (simp only: real_of_int_of_nat_eq)
    1.14  done
    1.15  
    1.16 -lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
    1.17 +lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> \<nat>"
    1.18  unfolding real_of_nat_def by (rule of_nat_in_Nats)
    1.19  
    1.20 -lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
    1.21 +lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> \<int>"
    1.22  unfolding real_of_nat_def by (rule Ints_of_nat)
    1.23  
    1.24  subsection \<open>The Archimedean Property of the Reals\<close>