equal
deleted
inserted
replaced
218 qed |
218 qed |
219 |
219 |
220 text \<open> |
220 text \<open> |
221 |
221 |
222 For more lemmas about the extended real numbers go to |
222 For more lemmas about the extended real numbers go to |
223 @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} |
223 @{file "~~/src/HOL/Analysis/Extended_Real_Limits.thy"} |
224 |
224 |
225 \<close> |
225 \<close> |
226 |
226 |
227 subsection \<open>Definition and basic properties\<close> |
227 subsection \<open>Definition and basic properties\<close> |
228 |
228 |