author nipkow Fri, 11 Jan 2019 18:41:50 +0100 changeset 69631 6c3e6038e74c parent 69630 aaa0b5f571e8 child 69632 7d02b7bee660
tuned headers
```--- 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"```
```--- 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"```
```--- 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```
```--- 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```