--- 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
--- 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:
--- 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 *)
--- 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:
--- 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>
--- 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*)
--- 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]