equal
deleted
inserted
replaced
216 by (auto intro!: eventually_INF1[of i] simp: eventually_principal) |
216 by (auto intro!: eventually_INF1[of i] simp: eventually_principal) |
217 done |
217 done |
218 qed |
218 qed |
219 |
219 |
220 text \<open> |
220 text \<open> |
221 |
221 For more lemmas about the extended real numbers see |
222 For more lemmas about the extended real numbers go to |
222 \<^file>\<open>~~/src/HOL/Analysis/Extended_Real_Limits.thy\<close>. |
223 @{file "~~/src/HOL/Analysis/Extended_Real_Limits.thy"} |
|
224 |
|
225 \<close> |
223 \<close> |
226 |
224 |
227 subsection \<open>Definition and basic properties\<close> |
225 subsection \<open>Definition and basic properties\<close> |
228 |
226 |
229 datatype ereal = ereal real | PInfty | MInfty |
227 datatype ereal = ereal real | PInfty | MInfty |