# HG changeset patch
# User wenzelm
# Date 1442694733 -7200
# Node ID a5674da43c2bb9c47bad61711916326febe79463
# Parent  413075a38b9e3d84aa58f0d825a9165d3146b761
eliminated hard tabs;

diff -r 413075a38b9e -r a5674da43c2b src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sat Sep 19 22:20:08 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sat Sep 19 22:32:13 2015 +0200
@@ -3166,8 +3166,8 @@
     and g: "valid_path g"
     and pag: "path_image g \<subseteq> s"
   shows "\<exists>L. 0 < L \<and>
-	     (\<forall>f B. f holomorphic_on s \<and> (\<forall>z \<in> s. norm(f z) \<le> B)
-		     \<longrightarrow> norm(path_integral g f) \<le> L*B)"
+       (\<forall>f B. f holomorphic_on s \<and> (\<forall>z \<in> s. norm(f z) \<le> B)
+         \<longrightarrow> norm(path_integral g f) \<le> L*B)"
 proof -
 have "path g" using g
   by (simp add: valid_path_imp_path)
@@ -3182,7 +3182,7 @@
   apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function)
   done
 then obtain p' where p': "polynomial_function p'"
-	       "\<And>x. (p has_vector_derivative (p' x)) (at x)"
+         "\<And>x. (p has_vector_derivative (p' x)) (at x)"
   using has_vector_derivative_polynomial_function by force
 then have "bounded(p' ` {0..1})"
   using continuous_on_polymonial_function