# HG changeset patch
# User nipkow
# Date 1547842966 -3600
# Node ID aeceb14f387a671b5d3009780e800c0d3d78bcd6
# Parent  94284d4dab987b0a3048c36f1c74842bc7d62b65# Parent  32eeb55d4bf3032eab81c66cb7a8172d17521e37
resolved conflict

diff -r 94284d4dab98 -r aeceb14f387a src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 17 17:50:01 2019 -0500
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Jan 18 21:22:46 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
diff -r 94284d4dab98 -r aeceb14f387a src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Jan 17 17:50:01 2019 -0500
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Jan 18 21:22:46 2019 +0100
@@ -15,7 +15,7 @@
 lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
   by auto
 
-subsubsection \<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,14 @@
 
 subsection \<open>Finite product spaces\<close>
 
+<<<<<<< local
 subsubsection \<open>Products\<close>
 
+||||||| base
+subsubsection%important \<open>Products\<close>
+
+=======
+>>>>>>> other
 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))"