--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -181,7 +181,7 @@
proof -
have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^sub>E j\<in>{..i}. E j))"
using E E[THEN sets.sets_into_space]
- by (auto simp: prod_emb_def Pi_iff extensional_def) blast
+ by (auto simp: prod_emb_def Pi_iff extensional_def)
with E show ?thesis by auto
qed
@@ -194,7 +194,7 @@
using E by (simp add: measure_PiM_emb)
moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
using E E[THEN sets.sets_into_space]
- by (auto simp: prod_emb_def extensional_def Pi_iff) blast
+ by (auto simp: prod_emb_def extensional_def Pi_iff)
moreover have "range ?E \<subseteq> sets S"
using E by auto
moreover have "decseq ?E"