# HG changeset patch
# User wenzelm
# Date 1492611969 -7200
# Node ID 587433a18053c486a855c97f9cc0772bb273efdf
# Parent  9fd620f2fa7db10b1578eeb18861754bae2efa55
tuned imports;

diff -r 9fd620f2fa7d -r 587433a18053 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>
diff -r 9fd620f2fa7d -r 587433a18053 src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Wed Apr 19 16:25:26 2017 +0200
+++ b/src/HOL/Library/Old_Datatype.thy	Wed Apr 19 16:26:09 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums\<close>
 
 theory Old_Datatype
-imports "../Main"
+imports Main
 keywords "old_datatype" :: thy_decl
 begin