| changeset 63627 | 6ddb43c6b711 |
| parent 63540 | f8652d0534fa |
| child 63680 | 6e1e8b5abbfa |
--- a/src/HOL/Library/Extended_Real.thy Fri Aug 05 18:34:57 2016 +0200 +++ b/src/HOL/Library/Extended_Real.thy Mon Aug 08 14:13:14 2016 +0200 @@ -220,7 +220,7 @@ text \<open> For more lemmas about the extended real numbers go to - @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} + @{file "~~/src/HOL/Analysis/Extended_Real_Limits.thy"} \<close>