src/HOL/Probability/Discrete_Topology.thy
```     1.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Tue Mar 05 15:43:13 2013 +0100
1.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Tue Mar 05 15:43:14 2013 +0100
1.3 @@ -50,15 +50,13 @@
1.4
1.5  instance discrete :: (countable) second_countable_topology
1.6  proof
1.7 -  let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
1.8 -  have "topological_basis ?B"
1.9 -  proof (intro topological_basisI)
1.10 -    fix x::"'a discrete" and O' assume "open O'" "x \<in> O'"
1.11 -    thus "\<exists>B'\<in>range (\<lambda>n. {from_nat n}). x \<in> B' \<and> B' \<subseteq> O'"
1.12 -      by (auto intro: exI[where x="to_nat x"])
1.13 -  qed (simp add: open_discrete_def)
1.14 +  let ?B = "range (\<lambda>n::'a discrete. {n})"
1.15 +  have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})"
1.16 +    by (intro generate_topology_Union) (auto intro: generate_topology.intros)
1.17 +  then have "open = generate_topology ?B"
1.18 +    by (auto intro!: ext simp: open_discrete_def)
1.19    moreover have "countable ?B" by simp
1.20 -  ultimately show "\<exists>B::'a discrete set set. countable B \<and> topological_basis B" by blast
1.21 +  ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast
1.22  qed
1.23
1.24  instance discrete :: (countable) polish_space ..
```