src/HOL/Probability/Fin_Map.thy
 changeset 50881 ae630bab13da parent 50251 227477f17c26 child 51104 59b574c6f803
```--- a/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 17:29:04 2013 +0100
@@ -1045,7 +1045,7 @@
lemma product_open_generates_sets_PiF_single:
assumes "I \<noteq> {}"
assumes [simp]: "finite I"
-  shows "sets (PiF {I} (\<lambda>_. borel::'b::countable_basis_space measure)) =
+  shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
proof -
from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
@@ -1064,7 +1064,7 @@
lemma product_open_generates_sets_PiM:
assumes "I \<noteq> {}"
assumes [simp]: "finite I"
-  shows "sets (PiM I (\<lambda>_. borel::'b::countable_basis_space measure)) =
+  shows "sets (PiM I (\<lambda>_. borel::'b::second_countable_topology measure)) =
sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
proof -
from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this```