src/HOL/Analysis/Inner_Product.thy

--- a/src/HOL/Analysis/Inner_Product.thy	Wed Apr 19 16:25:26 2017 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy	Wed Apr 19 16:26:09 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Inner Product Spaces and the Gradient Derivative\<close>
 
 theory Inner_Product
-imports "~~/src/HOL/Complex_Main"
+imports Complex_Main
 begin
 
 subsection \<open>Real inner product spaces\<close>