# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1565966888 -3600
# Node ID d18195a7c32f4a8f77ce263a048c0a119125b992
# Parent  87dffe9700bdfc984ed7f8b1980260501a958396
Fixed brace matching (plus some whitespace cleanup)

diff -r 87dffe9700bd -r d18195a7c32f src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Fri Aug 16 12:53:47 2019 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy	Fri Aug 16 15:48:08 2019 +0100
@@ -10,7 +10,7 @@
 
 subsection \<open>Equiintegrability\<close>
 
-text\<open>The definition here only really makes sense for an elementary set. 
+text\<open>The definition here only really makes sense for an elementary set.
      We just use compact intervals in applications below.\<close>
 
 definition\<^marker>\<open>tag important\<close> equiintegrable_on (infixr "equiintegrable'_on" 46)
@@ -27,7 +27,7 @@
 lemma equiintegrable_on_sing [simp]:
      "{f} equiintegrable_on cbox a b \<longleftrightarrow> f integrable_on cbox a b"
   by (simp add: equiintegrable_on_def has_integral_integral has_integral integrable_on_def)
-    
+
 lemma equiintegrable_on_subset: "\<lbrakk>F equiintegrable_on I; G \<subseteq> F\<rbrakk> \<Longrightarrow> G equiintegrable_on I"
   unfolding equiintegrable_on_def Ball_def
   by (erule conj_forward imp_forward all_forward ex_forward | blast)+
@@ -401,7 +401,7 @@
     using assms
     apply (auto simp: equiintegrable_on_def)
     apply (rule integrable_eq)
-    by auto 
+    by auto
 qed
 
 subsection\<open>Subinterval restrictions for equiintegrable families\<close>
@@ -1432,9 +1432,9 @@
       have *: "norm (h x) \<le> norm (f x)"
         if "h \<in> insert f (\<Union>c d. {?g B c d})" "x \<in> cbox a b" for h x
         using that by auto
-      have "(\<Union>i\<in>Basis. 
-                \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>i\<in>Basis. \<Union>\<psi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<psi> then h x else 0}). 
-                {\<lambda>x. if \<xi> \<le> x \<bullet> i then h x else 0}) 
+      have "(\<Union>i\<in>Basis.
+                \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>i\<in>Basis. \<Union>\<psi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<psi> then h x else 0}).
+                {\<lambda>x. if \<xi> \<le> x \<bullet> i then h x else 0})
              equiintegrable_on cbox a b"
       proof (rule equiintegrable_halfspace_restrictions_ge [where f=f])
         show "insert f (\<Union>i\<in>Basis. \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}).
@@ -1443,13 +1443,13 @@
           using insert.prems apply auto
           done
         show"norm(h x) \<le> norm(f x)"
-          if "h \<in> insert f (\<Union>i\<in>Basis. \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<xi> then h x else 0})" 
+          if "h \<in> insert f (\<Union>i\<in>Basis. \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<xi> then h x else 0})"
              "x \<in> cbox a b" for h x
           using that by auto
       qed auto
-      then have "insert f (\<Union>i\<in>Basis. 
-                \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>i\<in>Basis. \<Union>\<psi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<psi> then h x else 0}). 
-                {\<lambda>x. if \<xi> \<le> x \<bullet> i then h x else 0}) 
+      then have "insert f (\<Union>i\<in>Basis.
+                \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>i\<in>Basis. \<Union>\<psi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<psi> then h x else 0}).
+                {\<lambda>x. if \<xi> \<le> x \<bullet> i then h x else 0})
              equiintegrable_on cbox a b"
         by (blast intro: f equiintegrable_on_insert)
       then show ?case
@@ -1469,7 +1469,7 @@
   show ?thesis
     by (rule equiintegrable_on_subset [OF * [OF subset_refl]]) (auto simp: mem_box)
 qed
-  
+
 
 
 subsection\<open>Continuity of the indefinite integral\<close>
@@ -1935,7 +1935,7 @@
     proof (cases "g ?\<mu> \<ge> y")
       case True
       then obtain \<zeta> where \<zeta>: "\<And>x. g x \<ge> y \<longleftrightarrow> x \<ge> \<zeta>"
-        by (metis g lower order.trans)  \<comment> \<open>in fact y is @{term ?\<mu>}}\<close>
+        by (metis g lower order.trans)  \<comment> \<open>in fact y is @{term ?\<mu>}\<close>
       then show ?thesis
         by (force simp: \<zeta>)
     next
@@ -2010,7 +2010,7 @@
         proof (cases "g ?\<mu> \<ge> y")
           case True
           then obtain \<zeta> where \<zeta>: "\<And>x. g x \<ge> y \<longleftrightarrow> x \<ge> \<zeta>"
-            by (metis g lower order.trans)  \<comment> \<open>in fact y is @{term ?\<mu>}}\<close>
+            by (metis g lower order.trans)  \<comment> \<open>in fact y is @{term ?\<mu>}\<close>
           then show ?thesis
             by (force simp: \<zeta>)
         next
@@ -2205,7 +2205,7 @@
     and "((\<lambda>x. g x * f x) has_integral (g a * integral {a..c} f + g b * integral {c..b} f)) {a..b}"
 proof -
   have gab: "g a \<le> g b"
-    using \<open>a \<le> b\<close> g by blast 
+    using \<open>a \<le> b\<close> g by blast
   then consider "g a < g b" | "g a = g b"
     by linarith
   then show thesis
@@ -2270,4 +2270,4 @@
 
 
 end
-  
+