equal
deleted
inserted
replaced
248 const_syntax (xsymbols) |
248 const_syntax (xsymbols) |
249 Reals ("\<real>") |
249 Reals ("\<real>") |
250 |
250 |
251 lemma of_real_in_Reals [simp]: "of_real r \<in> Reals" |
251 lemma of_real_in_Reals [simp]: "of_real r \<in> Reals" |
252 by (simp add: Reals_def) |
252 by (simp add: Reals_def) |
|
253 |
|
254 lemma of_int_in_Reals [simp]: "of_int z \<in> Reals" |
|
255 by (subst of_real_of_int_eq [symmetric], rule of_real_in_Reals) |
|
256 |
|
257 lemma of_nat_in_Reals [simp]: "of_nat n \<in> Reals" |
|
258 by (subst of_real_of_nat_eq [symmetric], rule of_real_in_Reals) |
253 |
259 |
254 lemma Reals_0 [simp]: "0 \<in> Reals" |
260 lemma Reals_0 [simp]: "0 \<in> Reals" |
255 apply (unfold Reals_def) |
261 apply (unfold Reals_def) |
256 apply (rule range_eqI) |
262 apply (rule range_eqI) |
257 apply (rule of_real_0 [symmetric]) |
263 apply (rule of_real_0 [symmetric]) |