# HG changeset patch
# User immler
# Date 1360769707 -3600
# Node ID 5dd7b89a16de92408476feb60a873b44cb135bf3
# Parent  358b27c56469837cc784ff881ad21ecbb6498f32
generalized

diff -r 358b27c56469 -r 5dd7b89a16de src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 13 16:35:07 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 13 16:35:07 2013 +0100
@@ -794,7 +794,7 @@
     finally show "y \<in> ball x e" by (auto simp: ball_def)
   qed (insert a b, auto simp: box_def)
 qed
- 
+
 lemma open_UNION_box:
   fixes M :: "'a\<Colon>euclidean_space set"
   assumes "open M" 
@@ -5796,7 +5796,7 @@
   show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
 qed
 
-instance ordered_euclidean_space \<subseteq> polish_space ..
+instance euclidean_space \<subseteq> polish_space ..
 
 text {* Intervals in general, including infinite and mixtures of open and closed. *}