# HG changeset patch # User nipkow # Date 1547843773 -3600 # Node ID b18353d3fe1ab12e22c1ed9660a76a14460c6987 # Parent aeceb14f387a671b5d3009780e800c0d3d78bcd6 resolved conflict diff -r aeceb14f387a -r b18353d3fe1a src/HOL/Analysis/Finite_Product_Measure.thy --- 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 \Finite product spaces\ -<<<<<<< local -subsubsection \Products\ - -||||||| base -subsubsection%important \Products\ - -======= ->>>>>>> other definition%important prod_emb where "prod_emb I M K X = (\x. restrict x K) -` X \ (\\<^sub>E i\I. space (M i))"