# HG changeset patch
# User nipkow
# Date 1547228510 -3600
# Node ID 6c3e6038e74cb605212ac8879f8b309fb15b86f2
# Parent  aaa0b5f571e83044fdeaf39880e46cf5c79c939d
tuned headers

diff -r aaa0b5f571e8 -r 6c3e6038e74c src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Fri Jan 11 11:35:16 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Jan 11 18:41:50 2019 +0100
@@ -482,7 +482,7 @@
   by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
 
 
-subsection \<open>Derivatives of local minima and maxima are zero.\<close>
+subsection \<open>Derivatives of local minima and maxima are zero\<close>
 
 lemma has_derivative_local_min:
   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
diff -r aaa0b5f571e8 -r 6c3e6038e74c src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Jan 11 11:35:16 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Jan 11 18:41:50 2019 +0100
@@ -120,7 +120,7 @@
   "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
   unfolding%unimportant prod_emb_def PiE_def by auto
 
-lemma%unimportant (*FIX ME needs a name *)
+lemma%unimportant
   shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
     and prod_emb_Un[simp]: "prod_emb M L K (A \<union> B) = prod_emb M L K A \<union> prod_emb M L K B"
     and prod_emb_Int: "prod_emb M L K (A \<inter> B) = prod_emb M L K A \<inter> prod_emb M L K B"
diff -r aaa0b5f571e8 -r 6c3e6038e74c src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Jan 11 11:35:16 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Jan 11 18:41:50 2019 +0100
@@ -1,3 +1,5 @@
+subsection%important \<open>Ordered Euclidean Space\<close>
+
 theory Ordered_Euclidean_Space
 imports
   Cartesian_Euclidean_Space
diff -r aaa0b5f571e8 -r 6c3e6038e74c src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Fri Jan 11 11:35:16 2019 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Fri Jan 11 18:41:50 2019 +0100
@@ -3,7 +3,7 @@
     Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
 *)
 
-section%important \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close>
+section \<open>Tagged Divisions for Henstock-Kurzweil Integration\<close>
 (*FIXME move together with Henstock_Kurzweil_Integration.thy  *)
 theory Tagged_Division
   imports Topology_Euclidean_Space