--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 16 17:03:31 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Fri Jan 18 21:20:14 2019 +0100
@@ -2,7 +2,7 @@
Some material by Jose Divasón, Tim Makarios and L C Paulson
*)
-section%important \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\<close>
+section%important \<open>Finite Cartesian Products of Euclidean Spaces\<close>
theory Cartesian_Euclidean_Space
imports Cartesian_Space Derivative
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Wed Jan 16 17:03:31 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Fri Jan 18 21:20:14 2019 +0100
@@ -15,7 +15,7 @@
lemma%unimportant case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
by auto
-subsubsection%unimportant \<open>More about Function restricted by \<^const>\<open>extensional\<close>\<close>
+subsection%unimportant \<open>More about Function restricted by \<^const>\<open>extensional\<close>\<close>
definition
"merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
@@ -111,8 +111,6 @@
subsection%important \<open>Finite product spaces\<close>
-subsubsection%important \<open>Products\<close>
-
definition%important prod_emb where
"prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))"