equal
deleted
inserted
replaced
258 have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)" |
258 have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)" |
259 by (simp only: of_real_eq_iff of_nat_eq_iff) |
259 by (simp only: of_real_eq_iff of_nat_eq_iff) |
260 thus "(of_nat m = (of_nat n::'a)) = (m = n)" |
260 thus "(of_nat m = (of_nat n::'a)) = (m = n)" |
261 by (simp only: of_real_of_nat_eq) |
261 by (simp only: of_real_of_nat_eq) |
262 qed |
262 qed |
|
263 |
|
264 instance real_field < field_char_0 .. |
263 |
265 |
264 |
266 |
265 subsection {* The Set of Real Numbers *} |
267 subsection {* The Set of Real Numbers *} |
266 |
268 |
267 definition |
269 definition |