| changeset 63680 | 6e1e8b5abbfa |
| parent 63627 | 6ddb43c6b711 |
| child 63882 | 018998c00003 |
--- a/src/HOL/Library/Extended_Real.thy Fri Aug 12 17:49:02 2016 +0200 +++ b/src/HOL/Library/Extended_Real.thy Fri Aug 12 17:53:55 2016 +0200 @@ -218,10 +218,8 @@ qed text \<open> - -For more lemmas about the extended real numbers go to - @{file "~~/src/HOL/Analysis/Extended_Real_Limits.thy"} - + For more lemmas about the extended real numbers see + \<^file>\<open>~~/src/HOL/Analysis/Extended_Real_Limits.thy\<close>. \<close> subsection \<open>Definition and basic properties\<close>