src/HOL/Analysis/Embed_Measure.thy
changeset 69768 7e4966eaf781
parent 69700 7a92cbec7030
child 70136 f03a01a18c6e
     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Thu Jan 31 09:30:15 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Jan 31 13:08:59 2019 +0000
     1.3 @@ -263,8 +263,6 @@
     1.4                  simp del: map_prod_simp
     1.5                  del: prod_fun_imageE) []
     1.6      apply auto []
     1.7 -    apply (subst image_insert)
     1.8 -    apply simp
     1.9      apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
    1.10      apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
    1.11      apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq