--- a/src/HOL/Analysis/Derivative.thy Fri Jan 11 22:55:02 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy Fri Jan 11 22:59:00 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"
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Fri Jan 11 22:55:02 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Fri Jan 11 22:59:00 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"
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Fri Jan 11 22:55:02 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Fri Jan 11 22:59:00 2019 +0100
@@ -1,10 +1,12 @@
+subsection%important \<open>Ordered Euclidean Space\<close>
+
theory Ordered_Euclidean_Space
imports
Cartesian_Euclidean_Space
"HOL-Library.Product_Order"
begin
-subsection%important \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
+text%important \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
--- a/src/HOL/Analysis/Tagged_Division.thy Fri Jan 11 22:55:02 2019 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy Fri Jan 11 22:59:00 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