--- a/src/HOL/Analysis/Linear_Algebra.thy Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
theory Linear_Algebra
imports
Euclidean_Space
- "~~/src/HOL/Library/Infinite_Set"
+ "HOL-Library.Infinite_Set"
begin
lemma linear_simps: