| changeset 66453 | cc19f7ca2ed6 |
| parent 66447 | a1f5c5c26fa6 |
| child 66456 | 621897f47fab |
--- a/src/HOL/Analysis/Summation_Tests.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Analysis/Summation_Tests.thy Fri Aug 18 20:47:47 2017 +0200 @@ -7,9 +7,9 @@ theory Summation_Tests imports Complex_Main - "~~/src/HOL/Library/Discrete" - "~~/src/HOL/Library/Extended_Real" - "~~/src/HOL/Library/Liminf_Limsup" + "HOL-Library.Discrete" + "HOL-Library.Extended_Real" + "HOL-Library.Liminf_Limsup" begin text \<open>