| changeset 66672 | 75694b28ef08 |
| parent 66466 | aec5d9c88d69 |
| child 68532 | f8b98d31ad45 |
--- a/src/HOL/Analysis/Summation_Tests.thy Sun Sep 17 17:37:40 2017 +0200 +++ b/src/HOL/Analysis/Summation_Tests.thy Sun Sep 17 21:46:17 2017 +0200 @@ -10,7 +10,7 @@ "HOL-Library.Discrete" "HOL-Library.Extended_Real" "HOL-Library.Liminf_Limsup" - "Extended_Real_Limits" + Extended_Real_Limits begin text \<open>