--- a/src/HOL/Analysis/Finite_Product_Measure.thy Fri Jan 18 21:22:46 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Fri Jan 18 21:36:13 2019 +0100
@@ -111,14 +111,6 @@
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))"