# HG changeset patch
# User wenzelm
# Date 1446565657 -3600
# Node ID 7c985fd653c50effa65bc33f19fc138a8b5e18a5
# Parent  313eca3fa84720998c0ba021ae57a0e173439bba
tuned imports;

diff -r 313eca3fa847 -r 7c985fd653c5 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Nov 03 16:35:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Nov 03 16:47:37 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
+imports Cartesian_Euclidean_Space
 begin
 
 
diff -r 313eca3fa847 -r 7c985fd653c5 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Nov 03 16:35:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Nov 03 16:47:37 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>Complex Transcendental Functions\<close>
 
 theory Complex_Transcendental
-imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
+imports Complex_Analysis_Basics
 begin
 
 lemma cmod_add_real_less:
diff -r 313eca3fa847 -r 7c985fd653c5 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Nov 03 16:35:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Nov 03 16:47:37 2015 +0100
@@ -6,7 +6,7 @@
 section \<open>Multivariate calculus in Euclidean space\<close>
 
 theory Derivative
-imports Brouwer_Fixpoint Operator_Norm "~~/src/HOL/Multivariate_Analysis/Uniform_Limit"
+imports Brouwer_Fixpoint Operator_Norm Uniform_Limit
 begin
 
 lemma netlimit_at_vector: (* TODO: move *)
diff -r 313eca3fa847 -r 7c985fd653c5 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 03 16:35:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 03 16:47:37 2015 +0100
@@ -8,7 +8,10 @@
 section \<open>Limits on the Extended real number line\<close>
 
 theory Extended_Real_Limits
-  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
+imports
+  Topology_Euclidean_Space
+  "~~/src/HOL/Library/Extended_Real"
+  "~~/src/HOL/Library/Indicator_Function"
 begin
 
 lemma compact_UNIV:
diff -r 313eca3fa847 -r 7c985fd653c5 src/HOL/Multivariate_Analysis/PolyRoots.thy
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Tue Nov 03 16:35:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Tue Nov 03 16:47:37 2015 +0100
@@ -1,12 +1,11 @@
-section \<open>polynomial functions: extremal behaviour and root counts\<close>
-
 (*  Author: John Harrison and Valentina Bruno
     Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
 *)
 
+section \<open>polynomial functions: extremal behaviour and root counts\<close>
+
 theory PolyRoots
 imports Complex_Main
-
 begin
 
 subsection\<open>Geometric progressions\<close>
diff -r 313eca3fa847 -r 7c985fd653c5 src/HOL/Multivariate_Analysis/Weierstrass.thy
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Nov 03 16:35:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Nov 03 16:47:37 2015 +0100
@@ -1,8 +1,7 @@
-section\<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
+section \<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
 
 theory Weierstrass
 imports Uniform_Limit Path_Connected
-
 begin
 
 (*FIXME: simplification changes to be enforced globally*)
diff -r 313eca3fa847 -r 7c985fd653c5 src/HOL/Multivariate_Analysis/ex/Approximations.thy
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Tue Nov 03 16:35:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Tue Nov 03 16:47:37 2015 +0100
@@ -1,7 +1,7 @@
 section \<open>Binary Approximations to Constants\<close>
 
 theory Approximations
-imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental"
+imports Complex_Transcendental
 begin
 
 declare of_real_numeral [simp]