updated imports;
authorwenzelm
Sun Sep 17 21:46:17 2017 +0200 (21 months ago)
changeset 6667275694b28ef08
parent 66671 41b64e53b6a1
child 66673 1e4450008c47
updated imports;
src/HOL/Analysis/Summation_Tests.thy
src/HOL/Data_Structures/Base_FDS.thy
     1.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Sun Sep 17 17:37:40 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Sun Sep 17 21:46:17 2017 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    "HOL-Library.Discrete"
     1.5    "HOL-Library.Extended_Real"
     1.6    "HOL-Library.Liminf_Limsup"
     1.7 -  "Extended_Real_Limits"
     1.8 +  Extended_Real_Limits
     1.9  begin
    1.10  
    1.11  text \<open>
     2.1 --- a/src/HOL/Data_Structures/Base_FDS.thy	Sun Sep 17 17:37:40 2017 +0200
     2.2 +++ b/src/HOL/Data_Structures/Base_FDS.thy	Sun Sep 17 21:46:17 2017 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4  theory Base_FDS
     2.5 -imports "../Library/Pattern_Aliases"
     2.6 +imports "HOL-Library.Pattern_Aliases"
     2.7  begin
     2.8  
     2.9  declare Let_def [simp]